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

Planning and Patching Proof

Alan Bundy

School of Informatics, University of Edinburgh
3.09 Appleton Tower, 11 Crichton Street, Edinburgh, EH8 9LE, UK
[e-mail]

Abstract. We describe proof planning: a technique for both describing
the hierarchical structure of proofs and then using this structure to guide
proof attempts. When such a proof attempt fails, these failures can be
analyzed and a patch formulated and applied. We also describe rippling:
a powerful proof method used in proof planning. We pose and answer a
number of common questions about proof planning and rippling.

1 Introduction

The Program Committee Chair of aisc-04 suggested that the published version

of my talk might be:

“ ... a short paper telling our audience what are the highlights of the
publication landscape for the subject of your presentation, what they
should read if they want to become better informed by systematic read-
ing, and why they should read the cited material (i.e. why it represents
the highlights), could have both immediate use and longer-term educa-
tional use for people who don't attend the conference but buy or read
the proceedings later.”

Below I have attempted to fulfill this brief. I have organized the paper as a
'Frequently Asked Questions' about proof planning, in general, and rippling, in
particular.

2 Proof Planning

2.1 Introduction

What Is Proof Planning? Proof planning is a technique for guiding the search
for a proof in automated theorem proving. A proof plan is an outline or plan
of a proof. To prove a conjecture, proof planning constructs a proof plan for a
proof and uses it to guide the construction of the proof itself. Proof planning
reduces the amount of search and curbs the combinatorial explosion. It also helps
pinpoint the cause of any proof attempt failure, suggesting a patch to facilitate
a renewed attempt.

The research reported in this paper was supported by EPSRC grant GR/S01771.