jtp.proof
Class Proof

java.lang.Object
  |
  +--jtp.proof.Proof

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

ReasoningStep

public class Proof

extends Object

implements Serializable

JTP's implementation of an InferenceWeb proof.

A Proof consists of a goal, bindings for free variables in the goal, the premises (subgoals) upon which the bound goal relies, proofs of the premises, and an inference representing the type of inference made at this step of the proof.

A Proof is actually a tree. The child nodes are accessed through the method getSubProofs().

See Also:

Serialized Form

Field Summary

protected Map	bindings
protected Object	goal
protected Inference	inference
protected List	subGoals
protected List	subProofs

Constructor Summary

protected	Proof()
	Proof(Object goal, List sps, Inference i, Map bindings)

Method Summary

Map	getBindings() A map of variable bindings in which the keys are free variables from the goal and the values are what the variables are bound to in the proof.
Object	getGoal() Returns the goal that this Proof proves.
Inference	getInference() The type of inference that this proof represents.
List	getSubGoals() Returns a List of subgoals, or premises, that this Proof relies upon to prove its goal.
List	getSubProofs() Returns a List of the direct child Proofs in the proof tree.
String	toString()
String	toString(String path, String prefix)

Methods inherited from class java.lang.Object

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

Field Detail

goal

protected Object goal

bindings

protected Map bindings

subGoals

protected List subGoals

subProofs

protected List subProofs

inference

protected Inference inference

Constructor Detail

Proof

protected Proof()

Proof

public Proof(Object goal,
             List sps,
             Inference i,
             Map bindings)

Parameters:

goal - the goal that this Proof proves

sps - a List of the subproofs that this proof of the goal is based on

i - the type of inference that this proof represents

bindings - a map in which the keys are Variables and the values are what the variables are bound to in this proof

Method Detail

getGoal

public Object getGoal()

Returns the goal that this Proof proves. Goals are most commonly CNFSentences, but they can be other Objects as well.

Returns:

the goal of this Proof

getSubProofs

public List getSubProofs()

Returns a List of the direct child Proofs in the proof tree. A proof in the subproof list at index i proves the goal in the subgoal list at index i.

Returns:

a list of the subproofs of this Proof

See Also:

getSubGoals()

getSubGoals

public List getSubGoals()

Returns a List of subgoals, or premises, that this Proof relies upon to prove its goal. If the subgoal list and the subproof list are equal in length, then this is a complete proof of the goal. If the subgoal list is longer, then this is a partial proof, and the remaining subgoals must be proven in order to prove the goal.

Returns:

a list of the subgoals of this Proof

See Also:

getSubProofs()

getInference

public Inference getInference()

The type of inference that this proof represents.

Returns:

the type of inference that this Proof performs

getBindings

public Map getBindings()

A map of variable bindings in which the keys are free variables from the goal and the values are what the variables are bound to in the proof.

Returns:

map of bindings for free variables in goal

See Also:

Variable

toString

public String toString()

Overrides:

toString in class Object

toString

public String toString(String path,
                       String prefix)