2026-08-16T17:30:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1737 2024-03-06T10:33:07Z ddc:004 open_access

Sound Lemma Generation for Proving Inductive Validity of Equations Aoto, Takahito Sound generalization inductive theorem automated theorem proving term rewriting 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Takahito Aoto 2008 Is Part Of LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2008.1737 urn:nbn:de:0030-drops-17379 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1737 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode