Automatic generation of simple lemmas from recursive definitions using decision procedures - Preliminary report

Deepak Kapur, Mahadevan Subramaniam

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

Using recent results on integrating induction schemes into decidable theories, a method for generating lemmas useful for reasoning about T-based function definitions is proposed. The method relies on terms in a decidable theory admitting a (finite set of) canonical form scheme(s) and ability to solve parametric equations relating two canonical form schemes with parameters. Using nontrivial examples, it is shown how the method can be used to automatically generate many simple lemmas; these lemmas are likely to be found useful in automatically proving other nontrivial properties of T-based functions, thus unburdening the user of having to provide many simple intermediate lemmas. During the formalization of a problem, after a user inputs T-based definitions, the method can be employed in the background to explore a search space of possible conjectures which can be attempted, thus building a library of lemmas as well as false conjectures. This investigation was motivated by our attempts to automatically generate lemmas arising in proofs of generic, arbitrary data-width parameterized arithmetic circuits. The scope of applicability of the proposed method is broader, however, including generating proofs for proof-carrying codes, certification of proof-carrying code as well as in reasoning about distributed computation algorithms.

Original languageEnglish (US)
Pages (from-to)125-145
Number of pages21
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2896
StatePublished - Dec 1 2003

Fingerprint

Decision Procedures
Lemma
Canonical form
Networks (circuits)
Reasoning
Parametric equations
Certification
Arithmetic Circuits
Distributed Computation
Libraries
Formalization
Search Space
Finite Set
Proof by induction
Likely
Arbitrary
Term

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

@article{29b2dc0d11ed48ed8225db09511060a3,
title = "Automatic generation of simple lemmas from recursive definitions using decision procedures - Preliminary report",
abstract = "Using recent results on integrating induction schemes into decidable theories, a method for generating lemmas useful for reasoning about T-based function definitions is proposed. The method relies on terms in a decidable theory admitting a (finite set of) canonical form scheme(s) and ability to solve parametric equations relating two canonical form schemes with parameters. Using nontrivial examples, it is shown how the method can be used to automatically generate many simple lemmas; these lemmas are likely to be found useful in automatically proving other nontrivial properties of T-based functions, thus unburdening the user of having to provide many simple intermediate lemmas. During the formalization of a problem, after a user inputs T-based definitions, the method can be employed in the background to explore a search space of possible conjectures which can be attempted, thus building a library of lemmas as well as false conjectures. This investigation was motivated by our attempts to automatically generate lemmas arising in proofs of generic, arbitrary data-width parameterized arithmetic circuits. The scope of applicability of the proposed method is broader, however, including generating proofs for proof-carrying codes, certification of proof-carrying code as well as in reasoning about distributed computation algorithms.",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "2003",
month = "12",
day = "1",
language = "English (US)",
volume = "2896",
pages = "125--145",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Automatic generation of simple lemmas from recursive definitions using decision procedures - Preliminary report

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 2003/12/1

Y1 - 2003/12/1

N2 - Using recent results on integrating induction schemes into decidable theories, a method for generating lemmas useful for reasoning about T-based function definitions is proposed. The method relies on terms in a decidable theory admitting a (finite set of) canonical form scheme(s) and ability to solve parametric equations relating two canonical form schemes with parameters. Using nontrivial examples, it is shown how the method can be used to automatically generate many simple lemmas; these lemmas are likely to be found useful in automatically proving other nontrivial properties of T-based functions, thus unburdening the user of having to provide many simple intermediate lemmas. During the formalization of a problem, after a user inputs T-based definitions, the method can be employed in the background to explore a search space of possible conjectures which can be attempted, thus building a library of lemmas as well as false conjectures. This investigation was motivated by our attempts to automatically generate lemmas arising in proofs of generic, arbitrary data-width parameterized arithmetic circuits. The scope of applicability of the proposed method is broader, however, including generating proofs for proof-carrying codes, certification of proof-carrying code as well as in reasoning about distributed computation algorithms.

AB - Using recent results on integrating induction schemes into decidable theories, a method for generating lemmas useful for reasoning about T-based function definitions is proposed. The method relies on terms in a decidable theory admitting a (finite set of) canonical form scheme(s) and ability to solve parametric equations relating two canonical form schemes with parameters. Using nontrivial examples, it is shown how the method can be used to automatically generate many simple lemmas; these lemmas are likely to be found useful in automatically proving other nontrivial properties of T-based functions, thus unburdening the user of having to provide many simple intermediate lemmas. During the formalization of a problem, after a user inputs T-based definitions, the method can be employed in the background to explore a search space of possible conjectures which can be attempted, thus building a library of lemmas as well as false conjectures. This investigation was motivated by our attempts to automatically generate lemmas arising in proofs of generic, arbitrary data-width parameterized arithmetic circuits. The scope of applicability of the proposed method is broader, however, including generating proofs for proof-carrying codes, certification of proof-carrying code as well as in reasoning about distributed computation algorithms.

UR - http://www.scopus.com/inward/record.url?scp=0346325991&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0346325991&partnerID=8YFLogxK

M3 - Article

VL - 2896

SP - 125

EP - 145

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -