JTP API Documentation

jtp.modelim
Class ModelEliminationReasoner

java.lang.Object
  |
  +--java.beans.beancontext.BeanContextChildSupport
        |
        +--jtp.util.PropertyImporter
              |
              +--jtp.modelim.ModelEliminationReasoner
All Implemented Interfaces:
BeanContextChild, BeanContextServiceRevokedListener, BeanContextServicesListener, EventListener, Reasoner, Serializable

public class ModelEliminationReasoner
extends PropertyImporter
implements Reasoner

An asking control reasoner that works by decomposing goals into subgoals. Goals are passed to a ModelEliminationReasoner through the method process(java.lang.Object).

This reasoner passes goals to an AskingControlDispatcher, and the dispatcher returns proofs that may or may not be partial. If the proof returned from the AskingControlDispatcher is partial, the ModelEliminationReasoner attempts to find proofs for the unproven subgoals. Once all necessary subgoals have been proven, the ModelEliminationReasoner constructs the final proof and returns it from process.

This reasoner implements the model elimination procedure by automatically adding a LinearReductionReasoner to the AskingControlDispatcher. It also adds to the AskingControlDispatcher a reasoner that uses a DepthMonitor to cut off search when the current maximum depth is reached. An AncestorCycleCutReasoner is also added to the AskingControlDispatcher to improve search time.

A ModelEliminationReasoner is generally installed as the TheoremProver for an IterativeDeepening reasoner, and the two control reasoners are used in conjunction.

See Also:
Serialized Form

Nested Class Summary
protected  class ModelEliminationReasoner.ProofCollector
           
 
Field Summary
 
Fields inherited from class java.beans.beancontext.BeanContextChildSupport
beanContext, beanContextChildPeer, pcSupport, rejectedSetBCOnce, vcSupport
 
Constructor Summary
ModelEliminationReasoner()
           
 
Method Summary
 boolean acceptable(Object o)
          decides if the goal is suitable for being processed by this reasoner.
 Dispatcher getAskingDispatcher()
           
 DepthMonitor getDepthMonitor()
           
 Reasoner getIntermediateResultDispatcher()
           
 Tracer getTracer()
           
 ReasoningStepIterator process(Object goal)
          This method attempts to find proof for the goal.
 void setAskingDispatcher(Dispatcher v)
           
 void setDepthMonitor(DepthMonitor v)
           
 void setIntermediateResultDispatcher(Reasoner v)
           
 void setTracer(Tracer v)
           
 
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

ModelEliminationReasoner

public ModelEliminationReasoner()
Method Detail

getTracer

public Tracer getTracer()

setTracer

public void setTracer(Tracer v)

getAskingDispatcher

public Dispatcher getAskingDispatcher()

setAskingDispatcher

public void setAskingDispatcher(Dispatcher v)

getIntermediateResultDispatcher

public Reasoner getIntermediateResultDispatcher()

setIntermediateResultDispatcher

public void setIntermediateResultDispatcher(Reasoner v)

getDepthMonitor

public DepthMonitor getDepthMonitor()

setDepthMonitor

public void setDepthMonitor(DepthMonitor v)

process

public ReasoningStepIterator process(Object goal)
                              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:
goal - 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.

JTP API Documentation