Information Technology Reference

In-Depth Information

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

Search WWH ::

Custom Search