Information Technology Reference
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
Has Proof Planning Been Implemented? Yes, in the
, 1990] and
system at Edinburgh and the Omega system at
are the proof planners.
They constructs a customized tactic for a conjecture and then a proof checker,
, executes the tactic.
could be interfaced to any tactic-based theorem prover. To
test this assertion, we interfaced
to the Cambridge HOL theorem prover
, 1998]. We are currently building a proof planner, called IsaPlan-
ner, in Isabelle [Dixon & Fleuriot, 2003].
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,
. A survey of such applications can be found
in chapter 5 of [Bundy
Can Proof Planning Be Applied to Non-mathematical Domains? Yes.
We have had some success applying proof planning to game playing (Bridge
, 1992,Frank & Basin, 1998] and Go [Willmott
, 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.
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