Abstract
Otter-lambda is Otter modified by adding code to implement an algorithm for lambda unification. Otter is a resolution-based, clause-language first-order prover that accumulates deduced clauses and uses strategies to control the deduction and retention of clauses. This is the first time that such a first-order prover has been combined in one program with a unification algorithm capable of instantiating variables to lambda terms to assist in the deductions. The resulting prover has all the advantages of the proof-search algorithm of Otter (speed, variety of inference rules, excellent handling of equality) and also the power of lambda unification. We illustrate how these capabilities work well together by using Otter-lambda to find proofs by mathematical induction. Lambda unification instantiates the induction schema to find a useful instance of induction, and then Otter's first-order reasoning can be used to carry out the base case and induction step. If necessary, induction can be used for those, too. We present and discuss a variety of examples of inductive proofs found by Otter-lambda: some in pure Peano arithmetic, some in Peano arithmetic with defined predicates, some in theories combining algebra and the natural numbers, some involving algebraic simplification (used in the induction step) by simplification code from MathXpert, and some involving list induction instead of numerical induction. These examples demonstrate the feasibility and usefulness of adding lambda unification to a first-order prover.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem proving system for classical type theory. J. Autom. Reason. 16, 321–353 (1996)
Aubin, R.: Mechanizing structural induction, Part I: Formal system. Theor. Comput. Sci. 9, 329–345 (1979)
Aubin, R.: Mechanizing structural induction, Part II: Strategies. Theor. Comput. Sci. 9, 347–362 (1979)
Beeson, M.: Lambda logic. In: Basin, D., Rusinowitch, M. (eds.) Proceedings of Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4–8, 2004, vol. 3097 of Lecture Notes in Artificial Intelligence, pp. 460–474. Springer (2004)
Beeson, M.: Implicit typing in lambda logic. Presented at the ESHOL Workshop at LPAR-12 and available at the Otter-lambda website [7]. (Dec. 2005)
Beeson, M.: MathXpert calculus assistant, software available from (and described at) www.HelpWithMath.com
Beeson, M.: The Otter-\(\lambda\) website: http://www.MichaelBeeson.com/research/Otter-lambda/index.php
Boyer, R.S., Moore, JS.: A Computational Logic Handbook. Academic, Boston (1988)
Bundy, A.: The Automation of Proof by Mathematical Induction, Chapter 13 of [13].
Bundy, A., Van Harnelen, F., Horn, C., Smaill, A.: The Oyster–Clam system. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, vol. 449 of Lecture Notes in Artificial Intelligence, pp. 647–648. Springer (1990)
Kapur, D., Zhang, H.: An overview of Rewrite Rule Laboratory (RRL). J. Comput. Math. Appl. 29(2), 91–114 (1995)
McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, pp. 663–664. Springer, Berlin/Heidelberg (1990)
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. II. Elsevier Science B.V., Amsterdam (2001). Co-published in the U.S. and Canada by MIT Press, Cambridge, Massachusetts
Wick, C., McCune, W.: Automated reasoning about elementary point-set topology. J. Autom. Reason. 5(2), 239–255 (1989)
Wos, L., Pieper, G.: A Fascinating Country in the World of Computing. World Scientific, Singapore (1999)
Author information
Authors and Affiliations
Corresponding author
Additional information
Research supported by NSF grant number CCR-0204362.
Rights and permissions
About this article
Cite this article
Beeson, M. Mathematical Induction in Otter-Lambda. J Autom Reasoning 36, 311–344 (2006). https://doi.org/10.1007/s10817-006-9036-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-006-9036-z