Sound Lemma Generation for Proving Inductive Validity of Equations

Author Takahito Aoto

Thumbnail PDF


  • Filesize: 427 kB
  • 12 pages

Document Identifiers

Author Details

Takahito Aoto

Cite AsGet BibTex

Takahito Aoto. Sound Lemma Generation for Proving Inductive Validity of Equations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 13-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


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.
  • Sound generalization
  • inductive theorem
  • automated theorem proving
  • term rewriting


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads