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.
@InProceedings{aoto:LIPIcs.FSTTCS.2008.1737, author = {Aoto, Takahito}, title = {{Sound Lemma Generation for Proving Inductive Validity of Equations}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {13--24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-08-8}, ISSN = {1868-8969}, year = {2008}, volume = {2}, editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay, V}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1737}, URN = {urn:nbn:de:0030-drops-17379}, doi = {10.4230/LIPIcs.FSTTCS.2008.1737}, annote = {Keywords: Sound generalization, inductive theorem, automated theorem proving, term rewriting} }
Feedback for Dagstuhl Publishing