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.