I have described a divergence critic, a computer program which attempts to identify diverging proof attempts and to propose lemmas and generalizations which overcome the divergence. The divergence critic has proved very successful; it enables the system SPIKE to prove many theorems from the definitions alone. The divergence critic's success can be largely attributed to the power of the rippling heuristic. This heuristic was originally developed for proofs using explicit induction but has since found several other applications. Difference matching is used to identify accumulating term structure which is causing divergence. Lemmas and generalizations are then proposed to ripple this term structure out of the way. There are other types of divergence which could perhaps be recognized by the divergence critic. Further research is needed to identify such divergence patterns, isolate their causes and propose ways of fixing them. This research may take advantage of the close links between divergence patterns and particular types of generalization. For instance, it may be possible to identify specific divergence patterns with the need to generalize common subterms in the theorem being proved.

Fri Apr 12 12:14:22 BST 1996