Sound Lemma Generation for Proving Inductive Validity of Equations

13 years 8 months ago
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 o...
Takahito Aoto
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2008
Authors Takahito Aoto
Comments (0)