org.qedeq.kernel.bo.logic.proof.checker
Class ProofChecker1Impl

java.lang.Object
  org.qedeq.kernel.bo.logic.proof.checker.ProofChecker1Impl

All Implemented Interfaces:

ProofChecker

public class ProofChecker1Impl
extends java.lang.Object
implements ProofChecker

Formal proof checker for basic rules.

Author:

Michael Meyling

Constructor Summary

ProofChecker1Impl()
Constructor.

Method Summary

LogicalCheckExceptionList	checkProof(Element formula, FormalProofLineList proof, RuleChecker checker, ModuleContext moduleContext, ReferenceResolver resolver) Checks if a formal proof is ok.
LogicalCheckExceptionList	checkRule(Rule rule, ModuleContext context, RuleChecker checker, ReferenceResolver resolver) Checks if a rule declaration is ok for the proof checker.
protected ModuleContext	getCurrentContext() Get current context within original.
protected void	setLocationWithinModule(java.lang.String locationWithinModule) Set location information where are we within the original module.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ProofChecker1Impl

public ProofChecker1Impl()

Constructor.

Method Detail

checkRule

public LogicalCheckExceptionList checkRule(Rule rule,
                                           ModuleContext context,
                                           RuleChecker checker,
                                           ReferenceResolver resolver)

Description copied from interface: ProofChecker

Checks if a rule declaration is ok for the proof checker.

Specified by:

checkRule in interface ProofChecker

Parameters:

rule - Rule we want to use later on.

context - Location information rule declaration. Important for locating errors.

checker - Gets defined rule information.

resolver - Resolver for references.

Returns:

Collected errors if there are any. Not null.

checkProof

public LogicalCheckExceptionList checkProof(Element formula,
                                            FormalProofLineList proof,
                                            RuleChecker checker,
                                            ModuleContext moduleContext,
                                            ReferenceResolver resolver)

Description copied from interface: ProofChecker

Checks if a formal proof is ok. If there are any errors the returned list (which is always not null) has a size greater zero. Precondition is a well formed environment. So every formula must be well formed, every necessary operator and predicate and function must exist.

Specified by:

checkProof in interface ProofChecker

Parameters:

formula - Formula we want to proof.

proof - Check this formal proof.

checker - Gets defined rule information.

moduleContext - Location information of formal proof. Important for locating errors.

resolver - Resolver for references.

Returns:

Collected errors if there are any. Not null.

setLocationWithinModule

protected void setLocationWithinModule(java.lang.String locationWithinModule)

Set location information where are we within the original module.

Parameters:

locationWithinModule - Location within module.

getCurrentContext

protected final ModuleContext getCurrentContext()

Get current context within original.

Returns:

Current context.