** Next:** Introduction

# A Divergence Critic for Inductive Proof

**Toby Walsh **

toby@itc.it

IRST, Location Pantè di Povo

I38100 Trento, ITALY

### Abstract:

*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.
*

*toby@itc.it *

Mon Apr 29 11:51:33 BST 1996