Next: Conclusions Up: A Divergence Critic for Previous: Results

Related Work

Critics for monitoring the construction of proofs were first proposed by Ireland for the CLAM prover [13]. In this framework, failure of one of the proof methods automatically invokes a critic. Various critics for explicit induction have been developed that speculate missing lemmas, perform generalizations, look for suitable case splits, etc. As rippling plays a central role in CLAM's proof methods, many of the heuristics are similar to those described here [14]. There are, however, several significant differences. First, the divergence critic described here works in an implicit (and not an explicit) induction setting. Second, the divergence critic is not automatically invoked but must identify when the proof is failing. Third, the divergence critic is less specialized. These last two differences reflect the fact that critics in CLAM are usually associated with the failure of a particular precondition to a heuristic. The same divergence pattern can, by comparison, arise for many different reasons: the need to generalize variables apart, to generalize common subterms, to add a lemma, etc. Fourth, the divergence critic must use difference matching to annotate terms; in CLAM, terms are usually already appropriately annotated. Finally, the divergence critic is less tightly coupled to the the theorem prover's inference rules or heuristics. The critic can therefore exploit the strengths of the prover without needing to reason about the complex rules or heuristics being used. For instance, the divergence critic has no difficulty identifying divergence in complex situations like nested or mutual inductions. The critic also benefits from the powerful simplification rules used by SPIKE.

Divergence has been studied quite extensively in completion procedures. Two of the main novelties of the critic described here are the use of difference matching to identify divergence, and the use of rippling in the speculation of lemmas to overcome divergence. Dershowitz and Pinchover, by comparison, use most specific generalization to identify divergence patterns in the critical pairs produced by completion [11]. Kirchner uses generalization modulo an equivalence relation to recognise such divergence patterns [15]; meta-rules are then synthesized to describe infinite families of rules with some common structure. Thomas and Jantke use generalization and inductive inference to recognize divergence patterns and to replace infinite sequences of critical pairs by a finite number of generalizations [17]. Thomas and Watson use generalization to replace an infinite set of rules by a finite complete set with an enriched signature [18].

Generalization modulo an equivalence enables complex divergence patters to be identified. However, it is in general undecidable. Most specific generalization, by comparison, is more limited. It cannot recognize divergence patterns which give nested wave-fronts like, In addition, most specific generalization cannot identify term structure in wave-holes. For example, consider the divergence sequence of equations produced when SPIKE attempts to prove example 25 from Section 8,

Divergence analysis identifies term structure accumulating within the accumulator argument of ,

This annotated sequence is the unique maximal difference match. These annotations suggest the need for the wave rule, This rule allows the proof to go through without divergence. By comparison, most specific generalization seems to be unable to identify this rule. The most specific generalization of the left hand side of this sequence gives the term (or, ignoring the first term in the sequence, ). Most specific generalization cannot, however, identify the more useful pattern, .

NQTHM contains a simple test for divergence based on subsumption. For instance, on example 13 of the last section, NQTHM is unable to simplify the following subgoal in the step case of the proof,


        (EQUAL (ROT (LENGTH X) (APPEND X (LIST Z)))
               (CONS Z (ROT (LENGTH X) X))))
Note that this is the lemma speculated by the divergence critic. NQTHM generalizes (LENGTH X) in this subgoal giving the false conjecture,

        (EQUAL (ROT Y (APPEND X (LIST Z)))
               (CONS Z (ROT Y X))))
After several more attempts at induction and generalization, NQTHM realizes the proof is diverging since a subgoal is subsumed by its parent. As the proof is therefore about to loop, NQTHM gives up. No attempt is made to analyse the failed proof attempt to identify where it started to go wrong. In addition, subsumption is a very weak test for divergence, much weaker than tests based on difference matching or generalization. This subsumption test recognizes divergence on just a small number of the failed examples in the last section.



Next: Conclusions Up: A Divergence Critic for Previous: Results


toby@itc.it
Fri Apr 12 12:14:22 BST 1996