proof.type
Class Goal

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

public class Goal

extends java.lang.Object

A goal to be proved. This is an attempt at implementing the algorithm described in Dowek, Gilles. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287-315, June 1993.

Field Summary

java.util.Vector

subgoals Ways in which this subgoal could be proved.

Constructor Summary

Goal(Context c)
Constructor.

Method Summary

void	expand() Expand this subgoal, finding subgoals which would prove it.
void	expandToDepth(int depth) Expand this Goal to some depth.
void	expandToDepth(int depth, int maxHoles) Expand this Goal to some depth, with a bound on the number of holes in the Goal.
Term	getProofTerm(Term proofSoFar) Looks for a completed proof in subgoals.

Methods inherited from class java.lang.Object

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

Field Detail

subgoals

public java.util.Vector subgoals

Ways in which this subgoal could be proved. If any of these is a "success context" (that is, has no holes), then this Goal has been proved.

Constructor Detail

Goal

public Goal(Context c)

Constructor.

Parameters:

c - the Context we're trying to fill the gaps in.

Method Detail

expand

public void expand()

Expand this subgoal, finding subgoals which would prove it. This will set subgoals to a Vector of Steps, any one of which would suffice to prove this Goal.

expandToDepth

public void expandToDepth(int depth)

Expand this Goal to some depth.

expandToDepth

public void expandToDepth(int depth,
                          int maxHoles)

Expand this Goal to some depth, with a bound on the number of holes in the Goal.

Parameters:

depth - the depth to expand the Goal to

maxHoles - the maximum number of holes to allow in this Goal

getProofTerm

public Term getProofTerm(Term proofSoFar)

Looks for a completed proof in subgoals.

Parameters:

proofSoFar - the proof term so far

Returns:

a proof Term, or null if no proof has been found.