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

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

All Implemented Interfaces:

ReferenceResolver, ProofChecker

public class ProofChecker2Impl
extends java.lang.Object
implements ProofChecker, ReferenceResolver

Formal proof checker for basic rules and conditional proof.

Author:

Michael Meyling

Constructor Summary

ProofChecker2Impl()
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.
Element	getNormalizedFormula(Element element) Get formula in a normalized format.
Element	getNormalizedLocalProofLineReference(java.lang.String reference) Get local for proof line reference.
Element	getNormalizedReferenceFormula(java.lang.String reference) Get reference formula in a normalized format.
ModuleContext	getReferenceContext(java.lang.String reference) Module context for proof line reference.
boolean	isLocalProofLineReference(java.lang.String reference) Is this a local proof line reference?
boolean	isProvedFormula(java.lang.String reference) Check if a reference is a proved formula.
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

ProofChecker2Impl

public ProofChecker2Impl()

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.

getCurrentContext

protected final ModuleContext getCurrentContext()

Get current context within original.

Returns:

Current context.

setLocationWithinModule

protected void setLocationWithinModule(java.lang.String locationWithinModule)

Set location information where are we within the original module.

Parameters:

locationWithinModule - Location within module.

isProvedFormula

public boolean isProvedFormula(java.lang.String reference)

Description copied from interface: ReferenceResolver

Check if a reference is a proved formula.

Specified by:

isProvedFormula in interface ReferenceResolver

Parameters:

reference - Reference to axiom, definition or proposition.

Returns:

Reference has a proved formula.

getNormalizedReferenceFormula

public Element getNormalizedReferenceFormula(java.lang.String reference)

Description copied from interface: ReferenceResolver

Get reference formula in a normalized format.

Specified by:

getNormalizedReferenceFormula in interface ReferenceResolver

Parameters:

reference - Reference to axiom, definition or proposition.

Returns:

Already proved formula.

getNormalizedFormula

public Element getNormalizedFormula(Element element)

Description copied from interface: ReferenceResolver

Get formula in a normalized format.

Specified by:

getNormalizedFormula in interface ReferenceResolver

Parameters:

element - Local formula to normalize.

Returns:

Normalized formula.

isLocalProofLineReference

public boolean isLocalProofLineReference(java.lang.String reference)

Description copied from interface: ReferenceResolver

Is this a local proof line reference?

Specified by:

isLocalProofLineReference in interface ReferenceResolver

Parameters:

reference - Local proof line reference to check for.

Returns:

Is this a local proof line reference for the caller?

getNormalizedLocalProofLineReference

public Element getNormalizedLocalProofLineReference(java.lang.String reference)

Description copied from interface: ReferenceResolver

Get local for proof line reference.

Specified by:

getNormalizedLocalProofLineReference in interface ReferenceResolver

Parameters:

reference - Local proof line reference to check for.

Returns:

Local proof line for the caller. Might be null.

getReferenceContext

public ModuleContext getReferenceContext(java.lang.String reference)

Description copied from interface: ReferenceResolver

Module context for proof line reference.

Specified by:

getReferenceContext in interface ReferenceResolver

Parameters:

reference - Local proof line reference to check for.

Returns:

Local proof line reference for the caller. Might be null.