License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2008.1737
URN: urn:nbn:de:0030-drops-17379
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1737/
Go to the corresponding LIPIcs Volume Portal

Aoto, Takahito

Sound Lemma Generation for Proving Inductive Validity of Equations

pdf-format:
08004.AotoTakahito.1737.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{aoto:LIPIcs:2008:1737,
  author =	{Takahito Aoto},
  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 =	{Ramesh Hariharan and Madhavan Mukund and V Vinay},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/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}
}

Keywords: Sound generalization, inductive theorem, automated theorem proving, term rewriting
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2008
Date of publication: 05.12.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI