Abstract
Using recent results on integrating induction schemes into decidable theories, a method for generating lemmas useful for reasoning about \(\mathcal{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 \(\mathcal{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 \(\mathcal{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.
This research was partially supported by an NSF ITR award CCR-0113611.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge Univ. Pr., Cambridge (1998)
Boyer, R.S., Moore, J.: A Computational Logic. Academic Press, London (1979)
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A Heuristic for Guiding Inductive Proofs. Artificial Intelligence 62, 185–253 (1993)
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Harcourt/ Academic Press, London (2001)
Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469–484. Springer, Heidelberg (2001)
Giesl, J., Kapur, D.: Deciding Inductive Validity of Equations. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 17–31. Springer, Heidelberg (2003); An expanded version appeared as Technical Report AIB- 2003-03, 2003 is available from http://aib.informatik.rwth-aachen.de
Kapur, D., Narendran, P., Zhang, H.: Automating Inductionless Induction using Test Sets. Journal of Symbolic Computation 11(1-2), 81–111 (1991)
Kapur, D., Subramaniam, M.: New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. Journal of Automated Reasoning 16, 39–78 (1996)
Kapur, D., Subramaniam, M.: Mechanically verifying a family of multiplier circuits. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 135–146. Springer, Heidelberg (1996)
Kapur, D., Subramaniam, M.: Mechanical verification of adder circuits using powerlists. Journal of Formal Methods in System Design 13(2), 127–158 (1998)
Kapur, D., Subramaniam, M.: Extending Decision Procedures with Induction Schemes. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 324–345. Springer, Heidelberg (2000)
Kapur, D., Subramaniam, M.: Using an induction prover for verifying arithmetic circuits. Int. Journal of Software Tools for Technology Transfer 3(1), 32–65 (2000)
Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (RRL). Journal of Computer and Mathematics with Applications 29, 91–114 (1995)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1), 1–12 (1984)
Walther, C.: Mathematical Induction. In: Gabbay, Hogger, Robinson (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, Oxford University Press, Oxford (1994)
Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A Mechanizable Induction Principle for Equational Specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Subramaniam, M. (2003). Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures – Preliminary Report –. In: Saraswat, V.A. (eds) Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation. ASIAN 2003. Lecture Notes in Computer Science, vol 2896. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40965-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-40965-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20632-3
Online ISBN: 978-3-540-40965-6
eBook Packages: Springer Book Archive