jtp.modelim
Class AskingQueryProcessor

java.lang.Object
  |
  +--java.beans.beancontext.BeanContextChildSupport
        |
        +--jtp.util.PropertyImporter
              |
              +--jtp.modelim.AskingQueryProcessor

All Implemented Interfaces:

BeanContextChild, BeanContextServiceRevokedListener, BeanContextServicesListener, EventListener, FirstOrderLogicTranslator, Reasoner, Serializable, Translator

public class AskingQueryProcessor

extends PropertyImporter

implements Reasoner, FirstOrderLogicTranslator

Converts a complex query into a pair of query definition and query answer literal.

The model elimination theorem prover normally takes literals as queries. This reasoner deals with the rest of the queries. Suppose the query S is a general-form first-order logic sentence, and variables ?x1, ?x2, ... ?xN are all the free variables in S. Then if we add the sentence

     (<= ($Answer ?x1 ?x2 ?x3 ... ?xN) S)                  (*)
 

to the knowledge base, where $Answer is a relation symbol not occuring anywhere else in the KB, the literal ($Answer ?x1 ?x2 ?x3 ... ?xN) will have the same set of models as S. Such literal is called the answer literal for S.

This reasoner creates the sentence of the form (*) for a complex query S, and then reformulates S into the terms of its answer literal. The answer literal definition (*) is asserted into a reasoner that can be set by the setTellingReasoner(jtp.Reasoner) function. For example, it can be just the general-purpose reasoner of the system. Note: this implementation does not clean up the query definition from the KB. Therefore, if the general-purpose reasoner is used to hold the answer literal definitions, its size will grow as more queries are being translated.

See Also:

Serialized Form

Nested Class Summary

static class

AskingQueryProcessor.ReformulationProofStep

Field Summary

Fields inherited from class java.beans.beancontext.BeanContextChildSupport

beanContext, beanContextChildPeer, pcSupport, rejectedSetBCOnce, vcSupport

Constructor Summary

AskingQueryProcessor()
Constructs a new AskingQueryProcessor.

Method Summary

boolean	acceptable(Object o) decides if the goal is suitable for being processed by this reasoner.
Reasoner	getTellingReasoner()
FirstOrderLogicTranslator	getTranslator()
ReasoningStepIterator	process(Object o) This method attempts to find proof for the goal.
void	setTellingReasoner(Reasoner v) sets the reasoner that receives the assertions defining the answer literals.
void	setTranslator(FirstOrderLogicTranslator translator)
Object	translate(Object o)
CNFSentence	translate(String text) Translates a sentence into CNF.

Methods inherited from class jtp.util.PropertyImporter

getImportedProperties, initializeBeanContextResources, setImportedProperties

Methods inherited from class java.beans.beancontext.BeanContextChildSupport

addPropertyChangeListener, addVetoableChangeListener, firePropertyChange, fireVetoableChange, getBeanContext, getBeanContextChildPeer, isDelegated, releaseBeanContextResources, removePropertyChangeListener, removeVetoableChangeListener, serviceAvailable, serviceRevoked, setBeanContext, validatePendingSetBeanContext

Methods inherited from class java.lang.Object

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

Constructor Detail

AskingQueryProcessor

public AskingQueryProcessor()

Constructs a new AskingQueryProcessor.

Method Detail

getTranslator

public FirstOrderLogicTranslator getTranslator()

setTranslator

public void setTranslator(FirstOrderLogicTranslator translator)

getTellingReasoner

public Reasoner getTellingReasoner()

Returns:

the reasoner that receives the assertions defining the answer literals.

setTellingReasoner

public void setTellingReasoner(Reasoner v)

sets the reasoner that receives the assertions defining the answer literals. When a query is translated, the sentence defining its answer literal will be asserted into this reasoner. Note that these definitions have to be accessible to the theorem prover in order for the query to be successful, i.e. the answer literal definition has to be a part of the resulting KB.

Parameters:

v - the reasoner that receives the assertions defining the answer literals.

translate

public Object translate(Object o)

Specified by:

translate in interface Translator

translate

public CNFSentence translate(String text)

Description copied from interface: FirstOrderLogicTranslator

Translates a sentence into CNF.

Specified by:

translate in interface FirstOrderLogicTranslator

Parameters:

text - the string representation of a sentence.

Returns:

the sentence in CNF.

process

public ReasoningStepIterator process(Object o)
                              throws ReasoningException

Description copied from interface: Reasoner

This method attempts to find proof for the goal. It returns an enumeration of reasoning steps that correspond to alternative proofs for the goal. Consequently, the items of the enumeration can actually belong to different models of the goal sentence, and have incompatible variable assignments.

Example. A reasoner that performs unification of the goal with facts in a knowledge base can return the following enumeration for the goal (parent joe ?x):

1. A reasoning step proving (parent joe fred) with variable assignment ?x=fred,
2. A reasoning step proving (parent joe mary) with variable assignment ?x=mary.

Specified by:

process in interface Reasoner

Parameters:

o - the goal: either a query or an assertion

Returns:

the iterator of reasoning steps - proofs for the query, or consequences of the assertion.

ReasoningException

acceptable

public boolean acceptable(Object o)

Description copied from interface: Reasoner

decides if the goal is suitable for being processed by this reasoner. This method should be fast; if there are doubts as to whether a goal is acceptable, and it looks like determining it might take some time, the method should return true and let the process method figure it out.

Example. Many reasoners only process literals with certain predicates and arity. These reasoners will use those criteria to determine acceptability, for example a reasoner dealing with equality could accept goals that are:

1. Literals,
2. have = as their relation predicate,
3. have exactly two arguments.

Specified by:

acceptable in interface Reasoner

Returns:

true if the goal is suitable for this reasoner, false otherwise.