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

domains. However, you can certainly envisage a proof planning system which did
not contain a rippling method (the Saarbrucken Omega system, for instance) and
you can envisage using rippling, e.g. as a tactic, in a non-proof planning system.
So there is no necessary connection. For more on rippling see

3.

§

What Are the Scope and Limitations of Proof Planning? Acritical
evaluation of proof planning can be found in [Bundy, 2002].

2.2 Discovery and Learning

Is It Possible to Automate the Learning of Proof Plans? Proof plans
can be learnt from example proofs. In the case of equation-solving methods,
this was demonstrated in [Silver, 1985]; in the case of inductive proof methods it
was demonstrated in [Desimone, 1989]. Both projects used forms of explanation-
based generalization. We also have a current project on the use of data-mining
techniques (both probabilistic reasoning and genetic programming) to construct
tactics from large corpora of proofs, [Duncan , 2004].

The hardest aspect of learning proof plans is coming up with the key meta-
level concepts to describe the preconditions of the methods. An example of such
a meta-level concept is that of 'wave-front' idea used in rippling. We have not
made much progress on automating the learning of these.

et al

How Can Humans Discover Proof Plans? This is an art similar to the
skill used by a good mathematics teacher when analyzing a student's proof or
explaining a new method of proof to a class. The key is identifying the appro-
priate meta-level concepts to generalize from particular examples. Armed with
the right concepts, standard inductive learning techniques can form the right
generalization (see

2.2).

§

2.3 Drawbacks and Limitations

What Happens if the Attempt to Find a Proof Plan Fails? In certain
circumstances proof critics can suggest an appropriate patch to a partial proof
plan. Suppose the preconditions of a method succeed, but this method is un-
packed into a series of sub-methods one of which fails, i.e. the preconditions of
the sub-method fail. Critics are associated with some of these patterns of fail-
ure. For instance, one critic may fire if the first two preconditions of a method
succeed, but the last one fails. It will then suggest an appropriate patch for this
kind of failure, e.g. suggest the form of a missing lemma, or suggest generalizing
the conjecture. The patch is instituted and proof planning continues.
The original critics paper is [Ireland, 1992]. A more recent paper is
[Ireland & Bundy, 1996]. Two important application of critics are: discovering
loop invariants in the verification of imperative programs [Stark & Ireland, 1998];
and the correction of false conjectures [Monroy

et al , 1994].