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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R.S. Boyer and J S. Moore, A Computational Logic. ACM Monographs in Computer Science, 1979.
A. Bundy, A. Stevens, A. Ireland, and A. Smaill, “Rippling: A heuristic for guiding inductive proofs”, Artificial Intelligence, 62:185–253, 1993.
D.Basin and T.Walsh “Difference Matching”, In Proc. of CADE 11, D. Kapur (editor), LNAI 607, Springer Verlag 1992.
J.T.Hesketh “Using middle out reasoning to guide inductive theorem proving”, Ph.D thesis. University of Edinburgh 1991.
A. Ireland and A. Bundy, “Productive Use of Failure in Inductive Proof”, Edinburgh DAI Research Report No: 716. To appear on the Special Issue on Automation of Proof by Mathematical Induction, JAR.
A. Ireland “The use of planning critics in mechanizing inductive proofs”, In Proc. LPAR 92, A. Voronkov (editor), LNAI 624 Springer Verlag, 1992.
Deepak Kapur and M. Subramaniam “ Failure Analysis and its role in Generalization”, Manuscript under Preparation.
Deepak Kapur and M.Subramaniam “Lemma Discovery in Automated Induction”, Technical Report, CS Dept., SUNY April, 1995(an expanded version of this paper).
D. Kapur and H. Zhangt “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 1995, 91–114. Earlier descriptions in CADE-88 and RTA-89.
T. Walsh “A divergence critic”, In Proc. of CADE 12, A. Bundy (editor), LNAI 814, Springer Verlag 1994.
H. Zhang, D. Kapur, and M.S. Krishnamoorthy, “A mechanizable induction principle for equational specifications,” Proc. Ninth International Conference on Automated Deduction, E. Lusk and R. Overbeek (eds.), LNCS, Vol. 310, Springer-Verlag, Berlin, 1988, 250–265.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Subramaniam, M. (1996). Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_112
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_112
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive