Planning and Patching Proof - Artificial Intelligence and Symbolic Computation - page 27

Common patterns in proofs are identified and represented in computational
form as general-purpose tactics, i.e. programs for directing the proof search
process. These tactics are then formally specified with methods using a meta-
language. Standard patterns of proof failure and appropriate patches to the
failed proofs attempts are represented as critics. To form a proof plan for a
conjecture the proof planner reasons with these methods and critics. The proof
plan consists of a customized tactic for the conjecture, whose primitive actions
are the general-purpose tactics. This customized tactic directs the search of a
tactic-based theorem prover.
For a general, informal introduction to proof planning see [Bundy, 1991].
Proof planning was first introduced in [Bundy, 1988]. An earlier piece of
work that led to the development of proof planning was the use of meta-level in-
ference to guide equation solving, implemented in the Press system (see
[Sterling et al , 1989]).

Has Proof Planning Been Implemented? Yes, in the Oyster / Clam system

[Bundy et al , 1990] and λ Clam system at Edinburgh and the Omega system at

Saarbrucken [Benzmuller are the proof planners.

They constructs a customized tactic for a conjecture and then a proof checker,
such as

et al , 1997]. Clam and λ Clam

, executes the tactic.
In principle,

Oyster

could be interfaced to any tactic-based theorem prover. To
test this assertion, we interfaced

Clam

Clam to the Cambridge HOL theorem prover

[Boulton , 1998]. We are currently building a proof planner, called IsaPlan-

ner, in Isabelle [Dixon & Fleuriot, 2003].

et al

How Has Proof Planning Been Evaluated? One of the main domains
of application has been in inductive reasoning [Bundy, 2001], with applications
to software and hardware verification, synthesis and transformation, but it has
also been applied to co-induction [Dennis

, 2000], limit theorems, diagonal-
ization arguments, transfinite ordinals, summing series, equational reasoning,
meta-logical reasoning, algebra,

et al

etc . A survey of such applications can be found

in chapter 5 of [Bundy et al , 2005].

Can Proof Planning Be Applied to Non-mathematical Domains? Yes.
We have had some success applying proof planning to game playing (Bridge
[Frank

et al , 1992,Frank & Basin, 1998] and Go [Willmott et al , 2001]) and to

configuration problems [Lowe , 1998]. It is potentially applicable wherever

there are common patterns of reasoning. Proof planning can be used to match
the problem to the reasoning method in a process of meta-level reasoning. Proof
planning gives a clean separation between the factual and search control infor-
mation, which facilitates their independent modification.

et al

What Is the Relation Between Proof Planning and Rippling? Rippling
is a key method in our proof plans for induction. It is also useful in non-inductive