ubc.cs.JLog.Foundation
Class jProver

java.lang.Object
  extended by ubc.cs.JLog.Foundation.jProver
Direct Known Subclasses:
jDebugProver

public class jProver
extends java.lang.Object

This class implements a prolog proving engine. It uses two goal stacks to represent progress in the search tree. The goals goal stack stores goals that have yet to be evaluated. The proved goal stack stores goals that are already evaluated (i.e., the frontier).

The proving process takes a goal from the goals stack and attempts to prove it. If successful, any subgoals of the goal are pushed onto the goals stack and the goal to be proved is pushed onto the proved stack.the is the default goal stack implementation.

Author:
Glendon Holst

Field Summary
protected  jKnowledgeBase database
           
protected  iGoalStack goals
           
protected  iGoalStack proved
           
 
Constructor Summary
jProver(jKnowledgeBase kb)
          Construct a prover instance with a given jKnowledgeBase.
 
Method Summary
protected  iGoalStack createGoalsStack()
          Construct a goal stack for goals.
protected  iGoalStack createProvedStack()
          Construct a goal stack for proved.
protected  boolean internal_prove()
           
protected  boolean internal_retry()
           
 boolean prove(jPredicateTerms goal)
          Initiate a proof of the provided goal.
 boolean retry()
          Attempts to prove the previous goal in a different way than before.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

database

protected jKnowledgeBase database

goals

protected iGoalStack goals

proved

protected iGoalStack proved
Constructor Detail

jProver

public jProver(jKnowledgeBase kb)
Construct a prover instance with a given jKnowledgeBase.

Parameters:
kb - the knowledge base which attempted proofs are based upon.
Method Detail

prove

public boolean prove(jPredicateTerms goal)
Initiate a proof of the provided goal.

Parameters:
goal - the term to attempt to prove.
Returns:
true if the proof of goal succeeded, false otherwise.

retry

public boolean retry()
Attempts to prove the previous goal in a different way than before. Only call after the previous call to prove succeeded, and no call to retry have failed.

Returns:
true if the proof of goal succeeded, false otherwise.

internal_prove

protected boolean internal_prove()

internal_retry

protected boolean internal_retry()

createProvedStack

protected iGoalStack createProvedStack()
Construct a goal stack for proved. Subclasses can override this factory method to return goal stacks with different capabilities (but same interface).

Returns:
instance of iGoalStack.

createGoalsStack

protected iGoalStack createGoalsStack()
Construct a goal stack for goals. Subclasses can override this factory method to return goal stacks with different capabilities (but same interface).

Returns:
instance of iGoalStack.