T. Walsh (1996) "A Divergence Critic for Inductive Proof", Volume 4, pages 209-235

PDF | PostScript | HTML | doi:10.1613/jair.275

Inductive theorem provers often diverge. This paper describes a simple critic, a computer program which monitors the construction of inductive proofs attempting to identify diverging proof attempts. Divergence is recognized by means of a ``difference matching'' procedure. The critic then proposes lemmas and generalizations which ``ripple'' these differences away so that the proof can go through without divergence. The critic enables the theorem prover Spike to prove many theorems completely automatically from the definitions alone.

Click here to return to Volume 4 contents list