Next: Difference matching and Up: A Divergence Critic for Previous: A Divergence Critic for


Two key problems in inductive theorem proving are proposing lemmas and generalizations. A prover's divergence often suggests to the user an appropriate lemma or generalization that will enable the proof to go through without divergence. As a simple example, consider the theorem,

This is part of a simple program verification problem [11]. Addition and doubling are defined recursively by means of the rewrite rules,

where represents the successor of (that is, ). I have adopted the PROLOG convention of writing meta-variables like and in upper case.

The theorem prover SPIKE [5] fails to prove this theorem. The proof attempt begins with a simple one step induction on . The base case is trivial. In the step case, the induction hypothesis is, And the induction conclusion is, To ease presentation, variables in this paper are, as here, sometimes renamed from those introduced by SPIKE. This has no effect on the results as the prover and divergence critic both alpha convert variable names where necessary. Rewriting the induction conclusion with the recursive definitions of and + gives, The outermost successor functions on either side of the equality are now cancelled, The prover then fertilizes with the induction hypothesis on the left hand side, This equation cannot be simplified further so another induction is performed. Unfortunately, this generates the diverging sequence of subgoals,

The problem is that the prover repeatedly tries an induction on but is unable to simplify the successor functions that this introduces on the first argument position of +. The proof will go through without divergence if we have the rewrite rule, This rule ``ripples'' accumulating successor functions off the first argument position of +. This rewrite rule is derived from the lemma, This is the commuted version of the recursive definition of addition and is, coincidently, a generalization of the first subgoal. This lemma can be proved without divergence as the induction variable, occurs just in the second argument position of +.

In this paper I describe a simple ``divergence critic'', a computer program which attempts to automate this process. The divergence critic identifies when a proof attempt is diverging by means of a ``difference matching'' procedure. The critic then proposes lemmas and generalizations which hopefully allow the proof to go through without divergence. Although the critic is designed to work with the prover SPIKE, it should also work with other induction provers [19]. SPIKE is a rewrite based theorem prover for first order conditional theories. It contains powerful rules for case analysis, simplification and implicit induction using the notion of a test set. Unfortunately, as is the case with other inductive theorem provers, its attempts to prove many theorems diverge without an appropriate generalization or the addition of a suitable lemma.

In Section 2, I describe difference matching and rippling, the two key ideas at the heart of the divergence critic. I then outline how difference matching identifies the accumulating term structure which is causing divergence (Section 3). In Section 4 and 6, I show how lemmas are speculated which ``ripple'' this term structure out of the way. In Section 5, I describe the heuristics used in generalizing these lemmas. Finally, implementation and results are described in Sections 7 and 8.

Next: Difference matching and Up: A Divergence Critic for Previous: A Divergence Critic for
Fri Apr 12 12:14:22 BST 1996