A Divergence Critic for Inductive Proof
<|reference_start|>A Divergence Critic for Inductive Proof: 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.<|reference_end|>
@article{walsh1996a,
    title={A Divergence Critic for Inductive Proof},
    author={T. Walsh},
    journal={Journal of Artificial Intelligence Research, Vol 4, (1996),
  209-235},
    year={1996},
    archivePrefix={arXiv},
    eprint={cs/9604101},
    primaryClass={cs.AI}
}