proof.prove
Class Goal

java.lang.Object
  |
  +--proof.prove.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.

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.