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

In other circumstances, a subgoal may be reached to which no method or
critic is applicable. It may be possible to back-up to a choice point in the search,
i.e. a place where two or more methods or critics were applicable. However, the
search space defined by the methods and critics is typically much smaller than
the search space defined by the object-level rules and axioms; that is both the
strength and the weakness of proof planning. The total search space is cropped to
the portion where the proof is most likely to occur - reducing the combinatorial
explosion, but losing completeness. It is always possible to regain completeness
by supplementing the methods with a default, general-purpose exhaustive search
method, but some would regard this as a violation of the spirit of proof planning.
For more discussion of these points see [Bundy, 2002].

Is It Possible to Discover New Kinds of Proof in a Proof Planning Sys-
tem? Since general-purpose proof plans represent common patterns in proofs,
then, by definition, they cannot discover new kinds of proof. This limitation
could be overcome in several ways. One would be to include a default method
which invoked some general search technique. This might find a new kind of
proof by accident. Another might be to have meta-methods which constructed
new methods. For instance, a method for one domain might be applied to an-
other by generalizing its preconditions 1 . Or a method might be learnt from
an example proof (see

2.2). Proof plans might, for instance, be learnt from
proofs constructed by general search. For more discussion of these points see
[Bundy, 2002].

§

Isn't Totally Automated Theorem Proving Infeasible? For the foresee-
able future theorem provers will require human interaction to guide the search
for non-trivial proofs. Fortunately, proof planning is also useful in interactive
theorem provers. Proof plans facilitate the hierarchical organization of a partial
proof, assisting the user to navigate around it and understand its structure. They
also provide a language for chunking the proof and for describing the interre-
lation between the chunks. Interaction with a semi-automated theorem prover
can be based on this language. For instance, the user can: ask why a proof
method failed to apply; demand that a heuristic precondition is overridden; use
the analysis from proof critics to patch a proof; etc.
The XBarnacle system is an semi-automated theorem prover based on proof
planning [Lowe & Duncan, 1997]. There is also a version of XBarnacle with in-
teraction critics, where the user assists the prover to find lemmas and general-
izations [Jackson & Lowe, 2000].

Doesn't Proof Planning Promote Cheating by Permitting Ad Hoc
Adjustments to Enable a Prover to 'Discover' Particular Proofs? Not
if the recommended methodology is adopted. [Bundy, 1991] specifies a set of

1 Often new departures come in mathematics when mathematicians switch from one
area to another, bringing their proof methods with them.