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

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

All Implemented Interfaces:

ModuleServicePluginExecutor, ServiceCompleteness, ListVisitor, QedeqVisitor

public final class SimpleProofFinderExecutor
extends ControlVisitor
implements ModuleServicePluginExecutor

Finds simple formal proofs.

Author:

Michael Meyling

Method Summary

java.lang.Object	executePlugin(InternalModuleServiceCall call, java.lang.Object data) Execute plugin.
java.lang.String	getLocationDescription() Get location info from traverser.
void	visitEnter(Axiom axiom) Visit certain element.
void	visitEnter(FunctionDefinition definition) 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.
void	visitLeave(Rule rule) Visit certain element.

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

addError, addError, addWarning, getBlocked, getCurrentContext, getCurrentNumbers, getErrorList, getInternalServiceCall, getInterrupted, getKernelQedeqBo, getLocalRuleKey, 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, 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

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, 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(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.

visitLeave

public void visitLeave(Rule rule)

Description copied from interface: QedeqVisitor

Visit certain element. End of visit.

Specified by:

visitLeave in interface QedeqVisitor

Overrides:

visitLeave in class AbstractModuleVisitor

Parameters:

rule - End visit of this element.

getLocationDescription

public java.lang.String getLocationDescription()

Description copied from class: ControlVisitor

Get location info from traverser.

Specified by:

getLocationDescription in interface ModuleServicePluginExecutor

Specified by:

getLocationDescription in interface ServiceCompleteness

Overrides:

getLocationDescription in class ControlVisitor

Returns:

Location description.