Sound lemma generation for proving inductive validity of equations

Takahito Aoto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)

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 other characteristic argument positions so as to enlarge the scope of the technique.

Original languageEnglish
Title of host publicationFSTTCS 2008 - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Pages13-24
Number of pages12
Volume2
Publication statusPublished - 2008 Dec 1
Event28th International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008 - Bangalore, India
Duration: 2008 Dec 92008 Dec 11

Other

Other28th International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008
CountryIndia
CityBangalore
Period08/12/908/12/11

Keywords

  • Automated theorem proving
  • Inductive theorem
  • Sound generalization
  • Term rewriting

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Sound lemma generation for proving inductive validity of equations'. Together they form a unique fingerprint.

  • Cite this

    Aoto, T. (2008). Sound lemma generation for proving inductive validity of equations. In FSTTCS 2008 - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 2, pp. 13-24)