Lemma discovery in automating induction

Deepak Kapur, M. Subramaniam

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

22 Citations (Scopus)

Abstract

Speculating intermediate lemmas is one of the main reason of user interaction/guidance while mechanically attempting proofs by induction. An approach for generating intermediate lemmas is developed, and its effectiveness is demonstrated while proving properties of recursively defined functions. The approach is guided by the paradigm of attempting to generate a proof of the conclusion subgoal in an induction step by the application of an induction hypothesis (es). Generation of intermediate conjectures is motivated by attempts to find appropriate instantiations for non-induction variables in the main conjecture. In case, the main conjecture does not have any non-induction variables, such variables are introduced by attempting its generalization. A constraint based paradigm is proposed for guessing the missing side of an intermediate conjecture by identifying constraints on the term schemes introduced for the missing side. Definitions and properties of functions are judiciously used for generating instantiations and intermediate conjectures. Heuristics are identified for performing such analysis. The approach fails if appropriate instantiations of non-induction variables cannot be generated. Otherwise, proofs of intermediate conjectures are attempted and the proposed method is recursively applied. The method has proven to be surprisingly effective in speculating intermediate lemmas for tail-recursive programs.

Original languageEnglish (US)
Title of host publicationAutomated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
EditorsJohn K. Slaney, Michael A. McRobbie
PublisherSpringer Verlag
Pages538-552
Number of pages15
ISBN (Print)3540615113, 9783540615118
DOIs
StatePublished - Jan 1 1996
Event13th International Conference on Automated Deduction, CADE 1996 - New Brunswick, United States
Duration: Jul 30 1996Aug 3 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1104
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Automated Deduction, CADE 1996
CountryUnited States
CityNew Brunswick
Period7/30/968/3/96

Fingerprint

Lemma
Proof by induction
Paradigm
User Interaction
Guidance
Tail
Heuristics
Term

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1996). Lemma discovery in automating induction. In J. K. Slaney, & M. A. McRobbie (Eds.), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings (pp. 538-552). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_112

Lemma discovery in automating induction. / Kapur, Deepak; Subramaniam, M.

Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. ed. / John K. Slaney; Michael A. McRobbie. Springer Verlag, 1996. p. 538-552 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104).

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

Kapur, D & Subramaniam, M 1996, Lemma discovery in automating induction. in JK Slaney & MA McRobbie (eds), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1104, Springer Verlag, pp. 538-552, 13th International Conference on Automated Deduction, CADE 1996, New Brunswick, United States, 7/30/96. https://doi.org/10.1007/3-540-61511-3_112
Kapur D, Subramaniam M. Lemma discovery in automating induction. In Slaney JK, McRobbie MA, editors, Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1996. p. 538-552. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-61511-3_112
Kapur, Deepak ; Subramaniam, M. / Lemma discovery in automating induction. Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. editor / John K. Slaney ; Michael A. McRobbie. Springer Verlag, 1996. pp. 538-552 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d122acf621f3449f8bed553df1b31e1f,
title = "Lemma discovery in automating induction",
abstract = "Speculating intermediate lemmas is one of the main reason of user interaction/guidance while mechanically attempting proofs by induction. An approach for generating intermediate lemmas is developed, and its effectiveness is demonstrated while proving properties of recursively defined functions. The approach is guided by the paradigm of attempting to generate a proof of the conclusion subgoal in an induction step by the application of an induction hypothesis (es). Generation of intermediate conjectures is motivated by attempts to find appropriate instantiations for non-induction variables in the main conjecture. In case, the main conjecture does not have any non-induction variables, such variables are introduced by attempting its generalization. A constraint based paradigm is proposed for guessing the missing side of an intermediate conjecture by identifying constraints on the term schemes introduced for the missing side. Definitions and properties of functions are judiciously used for generating instantiations and intermediate conjectures. Heuristics are identified for performing such analysis. The approach fails if appropriate instantiations of non-induction variables cannot be generated. Otherwise, proofs of intermediate conjectures are attempted and the proposed method is recursively applied. The method has proven to be surprisingly effective in speculating intermediate lemmas for tail-recursive programs.",
author = "Deepak Kapur and M. Subramaniam",
year = "1996",
month = "1",
day = "1",
doi = "10.1007/3-540-61511-3_112",
language = "English (US)",
isbn = "3540615113",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "538--552",
editor = "Slaney, {John K.} and McRobbie, {Michael A.}",
booktitle = "Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings",

}

TY - GEN

T1 - Lemma discovery in automating induction

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1996/1/1

Y1 - 1996/1/1

N2 - Speculating intermediate lemmas is one of the main reason of user interaction/guidance while mechanically attempting proofs by induction. An approach for generating intermediate lemmas is developed, and its effectiveness is demonstrated while proving properties of recursively defined functions. The approach is guided by the paradigm of attempting to generate a proof of the conclusion subgoal in an induction step by the application of an induction hypothesis (es). Generation of intermediate conjectures is motivated by attempts to find appropriate instantiations for non-induction variables in the main conjecture. In case, the main conjecture does not have any non-induction variables, such variables are introduced by attempting its generalization. A constraint based paradigm is proposed for guessing the missing side of an intermediate conjecture by identifying constraints on the term schemes introduced for the missing side. Definitions and properties of functions are judiciously used for generating instantiations and intermediate conjectures. Heuristics are identified for performing such analysis. The approach fails if appropriate instantiations of non-induction variables cannot be generated. Otherwise, proofs of intermediate conjectures are attempted and the proposed method is recursively applied. The method has proven to be surprisingly effective in speculating intermediate lemmas for tail-recursive programs.

AB - Speculating intermediate lemmas is one of the main reason of user interaction/guidance while mechanically attempting proofs by induction. An approach for generating intermediate lemmas is developed, and its effectiveness is demonstrated while proving properties of recursively defined functions. The approach is guided by the paradigm of attempting to generate a proof of the conclusion subgoal in an induction step by the application of an induction hypothesis (es). Generation of intermediate conjectures is motivated by attempts to find appropriate instantiations for non-induction variables in the main conjecture. In case, the main conjecture does not have any non-induction variables, such variables are introduced by attempting its generalization. A constraint based paradigm is proposed for guessing the missing side of an intermediate conjecture by identifying constraints on the term schemes introduced for the missing side. Definitions and properties of functions are judiciously used for generating instantiations and intermediate conjectures. Heuristics are identified for performing such analysis. The approach fails if appropriate instantiations of non-induction variables cannot be generated. Otherwise, proofs of intermediate conjectures are attempted and the proposed method is recursively applied. The method has proven to be surprisingly effective in speculating intermediate lemmas for tail-recursive programs.

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

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

U2 - 10.1007/3-540-61511-3_112

DO - 10.1007/3-540-61511-3_112

M3 - Conference contribution

AN - SCOPUS:84957615401

SN - 3540615113

SN - 9783540615118

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 538

EP - 552

BT - Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings

A2 - Slaney, John K.

A2 - McRobbie, Michael A.

PB - Springer Verlag

ER -