×

Mathematical induction in Otter-lambda. (English) Zbl 1107.68093

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

RRL; NQTHM; MathXpert; TPS; OTTER
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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) · Zbl 0858.03017 · doi:10.1007/BF00252180
[2] Aubin, R.: Mechanizing structural induction, Part I: Formal system. Theor. Comput. Sci. 9, 329–345 (1979) · Zbl 0423.68050 · doi:10.1016/0304-3975(79)90034-3
[3] Aubin, R.: Mechanizing structural induction, Part II: Strategies. Theor. Comput. Sci. 9, 347–362 (1979) · Zbl 0423.68051 · doi:10.1016/0304-3975(79)90035-5
[4] 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) · Zbl 1127.03009
[5] 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)
[6] Beeson, M.: MathXpert calculus assistant, software available from (and described at) www.HelpWithMath.com
[7] Beeson, M.: The Otter- \(\lambda\) website: http://www.MichaelBeeson.com/research/Otter-lambda/index.php · Zbl 1107.68093
[8] Boyer, R.S., Moore, JS.: A Computational Logic Handbook. Academic, Boston (1988) · Zbl 0655.68117
[9] Bundy, A.: The Automation of Proof by Mathematical Induction, Chapter 13 of [13]. · Zbl 0994.03007
[10] 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)
[11] Kapur, D., Zhang, H.: An overview of Rewrite Rule Laboratory (RRL). J. Comput. Math. Appl. 29(2), 91–114 (1995) · Zbl 00718813 · doi:10.1016/0898-1221(94)00218-A
[12] McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, pp. 663–664. Springer, Berlin/Heidelberg (1990)
[13] 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
[14] Wick, C., McCune, W.: Automated reasoning about elementary point-set topology. J. Autom. Reason. 5(2), 239–255 (1989) · Zbl 0675.68049 · doi:10.1007/BF00243005
[15] Wos, L., Pieper, G.: A Fascinating Country in the World of Computing. World Scientific, Singapore (1999) · Zbl 1132.68300
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.