org.qedeq.kernel.bo.logic.proof.common
Interface ProofChecker

All Known Implementing Classes:

ProofChecker0Impl, ProofChecker1Impl, ProofChecker2Impl

public interface ProofChecker

A proof checker can check if a formal proof is correct.

Author:

Michael Meyling

Method Summary

LogicalCheckExceptionList	checkProof(Element formula, FormalProofLineList proof, RuleChecker checker, ModuleContext context, 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.

Method Detail

checkProof

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

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.

Parameters:

formula - Formula we want to proof.

proof - Check this formal proof.

checker - Gets defined rule information.

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

resolver - Resolver for references.

Returns:

Collected errors if there are any. Not null.

checkRule

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

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

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.