proof.type
Class Step

java.lang.Object
  |
  +--proof.type.Step

public class Step

extends java.lang.Object

One "step" in breaking down a proof, in which one hole gets substituted into (which may create other holes.)

Constructor Summary

Step(Context c, ExistBinding x, Context c1, Term s)
Constructor.

Method Summary

void	expandToDepth(int depth) Expand the subgoal to some depth.
Term	getProofTerm(Term proofSoFar) Get the proof of the goal, if possible.

Methods inherited from class java.lang.Object

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

Constructor Detail

Step

public Step(Context c,
            ExistBinding x,
            Context c1,
            Term s)

Constructor.

Method Detail

getProofTerm

public Term getProofTerm(Term proofSoFar)

Get the proof of the goal, if possible.

Parameters:

proofSoFar - the term being substituted into. At the top level, this will be the ExistBinding corresponding to the original goal. As we go through the tree, compose the substitutions (as described in Dowek's paper.)

Returns:

the proof term, or null if no proof has been found yet.

expandToDepth

public void expandToDepth(int depth)

Expand the subgoal to some depth.