Sound Lemma Generation for Proving Inductive Validity of Equations

Abstract

In many automated methods for proving inductive theorems, finding a
suitable generalization 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
incorrect conjecture are made, which is against the success and
efficiency 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
paper, 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 flexibilities to some of other characteristic argument
positions so as to enlarge the scope of the technique.