A Divergence Critic for Inductive Proof

TL;DR

This paper introduces a divergence critic for inductive theorem proving that detects divergence during proof construction and suggests lemmas to guide the proof to completion, significantly improving automation.

Contribution

It presents a simple critic that monitors and corrects divergence in inductive proofs, enabling more automatic theorem proving from definitions.

Findings

Enables Spike to prove many theorems automatically

Detects divergence using difference matching

Proposes lemmas to prevent divergence

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.