Generalization Discovery for Proofs by Induction

Several induction provers have been developed to automate inductive proofs (see for instance: Nqthm, RRL INKA, LP, SPIKE, CLAM-Oyster, ...). However, inductive theorem provers very often fail to terminate. A proof to go through requires eit her additional lemmas, a generalization, a suitable induction variable to induce upon , or a case split. The aim of this paper is to present a simple and powerful heuristic that allows to overcome, in many cases, the divergence of induction provers when working wit h conditional theories. We first provide a new definition of induction variables and then formalize a new transition rule for induction (named CGT-rule). The e ssential idea behind it is to propose a generalized form of the conclusion just before another induction is attempted and failure begins. This generalized form is based on the induction hypothesis and the current goal. CGT-rule enables to prove many theorems completely automatically from the functi ons definitions alone. We illustrate computer applications to the correctness pr oof of the insertion sorting algorithm and other programs computing on lists and numbers. All of them have never proved before without user-provided generaliza tions and/or lemmas.