org.qedeq.kernel.bo.service.logic
Class FormalProofCheckerExecutor

java.lang.Object
  org.qedeq.kernel.se.visitor.AbstractModuleVisitor
      org.qedeq.kernel.bo.service.basis.ControlVisitor
          org.qedeq.kernel.bo.service.logic.FormalProofCheckerExecutor

All Implemented Interfaces:

ReferenceResolver, RuleChecker, ModuleServicePluginExecutor, ServiceCompleteness, ListVisitor, QedeqVisitor

public final class FormalProofCheckerExecutor
extends ControlVisitor
implements ModuleServicePluginExecutor, ReferenceResolver, RuleChecker

Checks if all propositions have a correct formal proof.

Author:

Michael Meyling

Method Summary

protected void	addError(ModuleDataException me) Add exception to error collection.
protected void	addError(SourceFileException me) Add exception to error collection.
java.lang.Object	executePlugin(InternalModuleServiceCall call, java.lang.Object data) Execute plugin.
Element	getNormalizedFormula(Element formula) 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.
RuleKey	getRule(java.lang.String ruleName) Get maximum defined rule version.
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.
void	visitEnter(Axiom axiom) Visit certain element.
void	visitEnter(FunctionDefinition definition) Visit certain element.
void	visitEnter(Header header) Visit certain element.
void	visitEnter(InitialFunctionDefinition definition) Visit certain element.
void	visitEnter(InitialPredicateDefinition definition) Visit certain element.
void	visitEnter(PredicateDefinition definition) Visit certain element.
void	visitEnter(Proposition proposition) Visit certain element.
void	visitEnter(Rule rule) Visit certain element.
void	visitLeave(Axiom axiom) Visit certain element.
void	visitLeave(FunctionDefinition definition) Visit certain element.
void	visitLeave(InitialFunctionDefinition definition) Visit certain element.
void	visitLeave(InitialPredicateDefinition definition) Visit certain element.
void	visitLeave(PredicateDefinition definition) Visit certain element.
void	visitLeave(Proposition definition) Visit certain element.

Methods inherited from class org.qedeq.kernel.bo.service.basis.ControlVisitor

addWarning, getBlocked, getCurrentContext, getCurrentNumbers, getErrorList, getInternalServiceCall, getInterrupted, getKernelQedeqBo, getLocalRuleKey, getLocationDescription, getNodeBo, getNodeDisplay, getReference, getService, getServices, getTraverser, getVisitPercentage, getWarningList, hasErrors, hasNoErrors, setBlocked, setLocationWithinModule, traverse

Methods inherited from class org.qedeq.kernel.se.visitor.AbstractModuleVisitor

visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor

getInterrupted, getLocationDescription, getVisitPercentage

Method Detail

executePlugin

public java.lang.Object executePlugin(InternalModuleServiceCall call,
                                      java.lang.Object data)
                               throws InterruptException

Description copied from interface: ModuleServicePluginExecutor

Execute plugin.

Specified by:

executePlugin in interface ModuleServicePluginExecutor

Parameters:

call - Service call.

data - Process execution data.

Returns:

Plugin specific resulting object. Might be null.

Throws:

InterruptException - User canceled execution.

visitEnter

public void visitEnter(Header header)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

header - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitEnter

public void visitEnter(Axiom axiom)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

axiom - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(Axiom axiom)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

axiom - End visit of this element.

visitEnter

public void visitEnter(PredicateDefinition definition)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

definition - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(PredicateDefinition definition)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

definition - End visit of this element.

visitEnter

public void visitEnter(InitialPredicateDefinition definition)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

definition - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(InitialPredicateDefinition definition)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

definition - End visit of this element.

visitEnter

public void visitEnter(InitialFunctionDefinition definition)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

definition - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(InitialFunctionDefinition definition)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

definition - End visit of this element.

visitEnter

public void visitEnter(FunctionDefinition definition)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

definition - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(FunctionDefinition definition)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

definition - End visit of this element.

visitEnter

public void visitEnter(Proposition proposition)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

proposition - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

visitLeave

public void visitLeave(Proposition definition)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

definition - End visit of this element.

visitEnter

public void visitEnter(Rule rule)
                throws ModuleDataException

Description copied from interface: QedeqVisitor

Visit certain element. Begin of visit.

Specified by:

visitEnter in interface QedeqVisitor

Overrides:

visitEnter in class AbstractModuleVisitor

Parameters:

rule - Begin visit of this element.

Throws:

ModuleDataException - Major problem occurred.

addError

protected void addError(ModuleDataException me)

Description copied from class: ControlVisitor

Add exception to error collection.

Overrides:

addError in class ControlVisitor

Parameters:

me - Exception to be added.

addError

protected void addError(SourceFileException me)

Description copied from class: ControlVisitor

Add exception to error collection.

Overrides:

addError in class ControlVisitor

Parameters:

me - Exception to be added.

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 formula)

Description copied from interface: ReferenceResolver

Get formula in a normalized format.

Specified by:

getNormalizedFormula in interface ReferenceResolver

Parameters:

formula - 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?

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.

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.

getRule

public RuleKey getRule(java.lang.String ruleName)

Description copied from interface: RuleChecker

Get maximum defined rule version.

Specified by:

getRule in interface RuleChecker

Parameters:

ruleName - Name of rule.

Returns:

Maximum rule version. Might be null.