org.qedeq.kernel.bo.control
Class QedeqBoFormalLogicChecker

java.lang.Object
  org.qedeq.kernel.bo.visitor.AbstractModuleVisitor
      org.qedeq.kernel.bo.control.QedeqBoFormalLogicChecker

All Implemented Interfaces:

ClassOperatorExistenceChecker, EqualityOperatorExistenceChecker, ExistenceChecker, FunctionExistenceChecker, ListVisitor, PredicateExistenceChecker, QedeqVisitor

public final class QedeqBoFormalLogicChecker

extends AbstractModuleVisitor

implements ExistenceChecker

Checks if all formulas of a QEDEQ module are well formed.

Version:

$Revision: 1.2 $

Method Summary

static void	check(String globalContext, QedeqBo qedeq) Checks if all formulas of a QEDEQ module are well formed.
boolean	classOperatorExists() Check if the class operator is already defined.
boolean	equalityOperatorExists() Check if the equality operator is already defined.
boolean	functionExists(String name, int arguments) Check if a function is already defined.
ModuleContext	getCurrentContext() Get current context within original.
String	getEqualityOperator() Get equality operator.
protected Qedeq	getQedeqOriginal() Get original QEDEQ module.
boolean	predicateExists(String name, int arguments) Check if a predicate is already defined.
void	setLocationWithinModule(String locationWithinModule) Set location information where are we within the original module.
void	visitEnter(Axiom axiom) Visit certain element.
void	visitEnter(FunctionDefinition 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.

Methods inherited from class org.qedeq.kernel.bo.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, 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

Method Detail

check

public static void check(String globalContext,
                         QedeqBo qedeq)
                  throws ModuleDataException

Checks if all formulas of a QEDEQ module are well formed.

Parameters:

globalContext - Module location information.

qedeq - Basic QEDEQ module object.

Throws:

ModuleDataException - Major problem occured.

visitEnter

public final 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

Throws:

ModuleDataException

visitEnter

public final 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

Throws:

ModuleDataException

visitEnter

public final 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

Throws:

ModuleDataException

visitEnter

public final 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

Throws:

ModuleDataException

visitEnter

public final 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

Throws:

ModuleDataException

setLocationWithinModule

public void setLocationWithinModule(String locationWithinModule)

Set location information where are we within the original module.

Parameters:

locationWithinModule - Location within module.

getCurrentContext

public final ModuleContext getCurrentContext()

Get current context within original.

Returns:

Current context.

getQedeqOriginal

protected final Qedeq getQedeqOriginal()

Get original QEDEQ module.

Returns:

Original QEDEQ module.

predicateExists

public boolean predicateExists(String name,
                               int arguments)

Description copied from interface: PredicateExistenceChecker

Check if a predicate is already defined.

Specified by:

predicateExists in interface PredicateExistenceChecker

Parameters:

name - Predicate name.

arguments - Number of operands for the predicate.

Returns:

Predicate is defined.

functionExists

public boolean functionExists(String name,
                              int arguments)

Description copied from interface: FunctionExistenceChecker

Check if a function is already defined.

Specified by:

functionExists in interface FunctionExistenceChecker

Parameters:

name - Function name.

arguments - Number of operands for the function.

Returns:

Functions is defined.

classOperatorExists

public boolean classOperatorExists()

Description copied from interface: ClassOperatorExistenceChecker

Check if the class operator is already defined.

Specified by:

classOperatorExists in interface ClassOperatorExistenceChecker

Returns:

Class operator is defined.

equalityOperatorExists

public boolean equalityOperatorExists()

Description copied from interface: EqualityOperatorExistenceChecker

Check if the equality operator is already defined.

Specified by:

equalityOperatorExists in interface EqualityOperatorExistenceChecker

Returns:

Equality operator is already defined.

getEqualityOperator

public String getEqualityOperator()

Description copied from interface: EqualityOperatorExistenceChecker

Get equality operator. This is the operator string of a predicate.

Specified by:

getEqualityOperator in interface EqualityOperatorExistenceChecker

Returns:

Equality operator. Should be null if !EqualityOperatorExistenceChecker.equalityOperatorExists().