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.

- The
Use of Explicit Plans to Guide Inductive Proofs, A. Bundy in
R. Lusk and R. Overbeek (eds)
*Proceedings of the 9th Conference on Automated Deduction (CADE 9)*pp. 111-120, Springer-Verlag, 1988. - Proof
Planning, A. Bundy in B. Drabble (ed)
*Proceedings of the 3rd International Conference on AI Planning Systems, (AIPS) 1996*, pp. 261-267, 1996. - Proof Planning Methods as Schemas, A. Bundy and J. D. C. Richardson
- Logic
Program Synthesis in a Higher Order Setting D. Lacey,
J. D. C. Richardson and A. Smaill,
*Proceedings of the First International Conference on Computational Logic (CL2000)*, Lecture Notes in Computer Science 1861, pp 87-100, Springer-Verlag, 2000.

Alan Smaill Last modified: Tue Mar 1 17:55:58 GMT 2011