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.