Next: Results Up: A Divergence Critic for Previous: Transverse Wave Rules


The divergence critic described in the previous sections has been implemented in PROLOG. The system consists of 787 lines of code defining approximate 100 different PROLOG predicates. More recently a cut down version has been incorporated directly within the SPIKE system which is written in CAML LIGHT [7]. The output of SPIKE is parsed to generate input to the critic. The input consists of: the equations which the prover attempts to prove by induction; sort information (for the type checker and difference matcher); the recursive argument positions (for constructing primary terms); and the rewrite rules defining the theory (used by the conjecture disprover).

Figure 1 gives the divergence critic's output on the problem discussed in the introduction. Either of the proposed lemmas when used as a rewrite rule is adequate to fix divergence. In addition, the proposed lemmas are sufficiently simple to be proved automatically without introducing fresh divergence. The first lemma is a rewrite rule for moving accumulating successor functions from the first argument position of + to the top of the term tree. The second lemma is a transverse wave rule discussed in Section 6 for moving accumulating successor functions from the first argument position of + to the second argument position.

The critic is successful at identifying divergence and proposing appropriate lemmas and generalizations for a significant number of theorems. Divergence analysis is very quick on most examples. The divergence pattern is recognized usually in less than a second. Most of the time is spent looking for generalizations and refuting over-generalizations with the conjecture disprover. This usually takes between 1 and 100 seconds. Additional heuristics for preventing over-generalization and a more efficient implementation of the conjecture disprover would speed up the critic considerably.
Fri Apr 12 12:14:22 BST 1996