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

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

All Implemented Interfaces:

ProofChecker

public class ProofChecker0Impl
extends java.lang.Object
implements ProofChecker

Formal proof checker that don't allow any proof method.

Author:

Michael Meyling

Constructor Summary

ProofChecker0Impl()
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.

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofChecker0Impl

public ProofChecker0Impl()

Constructor.

Method Detail

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.

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.