Sound Lemma Generation for Proving Inductive Validity of Equations

In many automated methods for proving inductive theorems, nding a suitable gener- alization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the in- correct conjecture are made, which is against the success and efciency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called sound generalization, that avoids such an over-generalization. Their method guarantees that if the original conjecture is an inductive theorem then so is the obtained generalization. In this pa- per, we revise and extend their method. We restore a condition on one of the characteristic argument positions imposed in their previous paper and show that otherwise there exists a counterexample to their main theorem. We also relax a condition imposed in their framework and add some exibilities to some of other characteristic argument positions so as to enlarge the scope of the technique.