Next: Introduction

A Divergence Critic for Inductive Proof

Toby Walsh
IRST, Location Pantè di Povo
I38100 Trento, ITALY


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.
Mon Apr 29 11:51:33 BST 1996