is a tool for automated theorem proving in higher order domains. In particular specialises in proof using induction based on the rippling heuristic. is a higher-order version of CLAM. Both CLAM and use proof planning to guide the search for a proof
Proof planning was first suggested by Bundy. A proof plan is a proof of a theorem at some level of abstraction presented as a tree. Each node in this tree is justified by a tactic. The exact nature of these tactics is unspecified, they may be sequences of inference rules, programs for generating sequences of inferences or a further proof plan at some lower level of abstraction. In principle while the generation of the proof tree may have involved heuristics and (possibly) unsound inference steps, it can be justified by executing the tactics attached to the nodes.
A proof plan is generated using AI-style planning techniques (in this is basically depth-first search though there is no theoretical reason why this should be the case). The planning operators used by a proof planner are called proof methods these are defined by their pre- and post-conditions which are used by the planner to form the proof plan. Proof methods have been called partial tactic specifications - in theory the method's pre- and post-conditions describe (partially) the proof state before and after the application of their associated tactic in some meta-language. It is possible to be satisfied with a proof plan as a proof if you are prepared to accept the soundness of the methods - alternatively the tactics can be executed to produce a proof in some object logic as a sequence of axioms and inference rule applications (methods are only infrequently of a sufficiently low level to be considered as inference rule applications).
came about when it was decided that we would increasingly need to construct plans over a higher-order domain. This is particularly necessary for program synthesis where the synthesised program starts as an uninstantiated meta-variable, which is gradually instantiated by the proof steps, until a complete proof has been constructed, at which time the meta-variable is a complete program, and the proof is a verification proof that it satisfies its specification.