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. Introduction Two key problems in inductive theorem proving are proposing lemmas and generalizations. A prover s divergence often suggests to the user an appropriate lemma or generalization that will enable the proof to go through without divergence. As a simple example, consider the theorem, n . This is part of a simple program verification problem .