×

Sound lemma generation for proving inductive validity of equations. (English) Zbl 1248.68447

Hariharan, Ramesh (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2008), December 9–11, 2008, Bangalore, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-08-8). LIPIcs – Leibniz International Proceedings in Informatics 2, 13-24, electronic only (2008).
Summary: 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. P. Urso and E. Kounalis [Theor. Comput. Sci. 323, No. 1–3, 443–471 (2004; Zbl 1078.68141)] 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.
For the entire collection see [Zbl 1213.68039].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 1078.68141

Software:

RRL; InKa; ACL2
PDFBibTeX XMLCite
Full Text: DOI Link