Characteristics of de Bruijn's early proof checker Automath

• Autorzy: Geuvers Herman , Nederpelt Rob

Identyfikatory

DOI

10.3233/FI-222112

• Języki publikacji: EN

Abstrakty

EN

The 'mathematical language' Automath, conceived by N.G. de Bruijn in 1968, was the first theorem prover actually working and was used for checking many specimina of mathematical content. Its goals and syntactic ideas inspired Th. Coquand and G. Huet to develop the calculus of constructions, CC ([1]), which was one of the first widely used interactive theorem provers and forms the basis for the widely used Coq system ([2]). The original syntax of Automath ([3, 4]) is not easy to grasp. Yet, it is essentially based on a derivation system that is similar to the Calculus of Constructions ('CC'). The relation between the Automath syntax and CC has not yet been sufficiently described, although there are many references in the type theory community to Automath. In this paper we focus on the backgrounds and on some uncommon aspects of the syntax of Automath. We expose the fundamental aspects of a 'generic' Automath system, encapsulating the most common versions of Automath. We present this generic Automath system in a modern syntactic frame. The obtained system makes use of λD, a direct extension of CC with definitions described in [5].

Słowa kluczowe

EN

syntax of Automath

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 185, nr 4
• Strony: 313--336
• Opis fizyczny: Bibliogr. 29 poz., rys., tab.

Twórcy

autor

Geuvers Herman

• Radboud University Nijmegen and Eindhoven University of Technology, Nijmegen, The Netherlands.

autor

Nederpelt Rob

• Eindhoven University of Technology, Nijmegen, The Netherlands

Bibliografia

• [1] Coquand T, Huet G. The Calculus of Constructions. Information and Computation, 1988. 76:95-120. doi:10.1016/0890-5401(88)90005-3.
• [2] Coq Development Team. The Coq Proof Assistant, Reference Manual. coq.inria.fr/.
• [3] Bruijn, de NG. The mathematical language AUTOMATH, its usage and some of its extensions. In: Symposium on Automatic Demonstration, Versailles, 1968, volume 125 of Lecture Notes in Mathematics, pp. 29-61. Springer, 1970. Reprinted in [4], pp. 73-100.
• [4] Nederpelt RP, Geuvers JH, Vrijer, de RC. Selected Papers on Automath. Studies in logic and the foundations of mathematics. North-Holland, Elsevier, Netherlands, 1994. ISBN:0-444-89822-0.
• [5] Nederpelt RP, Geuvers JH. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014. ISBN:9781107036505. URL https://books.google.nl/books?id=wzTJBAAAQBAJ.
• [6] Bruijn, de NG. A survey of the project Automath. In: Seldin JP, Hindley JR (eds.), To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism, pp. 579-606. Academic Press Inc., United States. ISBN:0-12-349050-2, 1980.
• [7] Landau E. Grundlagen der Analysis. Leipzig (first ed.), Chelsea Publ. Comp. New York (1960, third ed.), 1930.
• [8] Benthem Jutting, van L. Checking Landau’s “Grundlagen” in the Automath system : Appendices 3 and 4 (The PN-lines; Excerpt for ”Satz 27”). In: Nederpelt RP, Geuvers JH, Vrijer, de RC (eds.), Selected Papers on Automath, Studies in Logic, pp. 763-780. North-Holland Publishing Company, Netherlands. ISBN:0-444-89822-0, 1994 (originally 1976).
• [9] Ja´skowski S. On the Rules of Suppositions in Formal Logic. Studia Logica, 1934. 1:5-32.
• [10] Fitch F. Symbolic Logic, An Introduction. The Ronald Press Company, 1952.
• [11] Standefer S. Translations Between Gentzen-Prawitz and Ja´skowski-Fitch Natural Deduction Proofs. Stud Logica, 2019. 107(6):1103-1134. doi:10.1007/s11225-018-9828-2.
• [12] Zandleven I. A verifying program for Automath. In: Nederpelt R, Geuvers J, Vrijer, de R (eds.), Selected Papers on Automath, Studies in Logic, pp. 783-804. North-Holland Publishing Company, Netherlands. ISBN:0-444-89822-0, 1994 (originally 1973).
• [13] Wiedijk F. A New Implementation of Automath. J. Autom. Reason., 2002. 29(3-4):365-387. doi:10.1023/A:1021983302516.
• [14] van Daalen D. A description of Automath and some aspects of its language theory. In: Nederpelt RP, Geuvers JH, Vrijer, de RC (eds.), Selected Papers on Automath, Studies in Logic, pp. 101-126. North-Holland Publishing Company, Netherlands. ISBN:0-444-89822-0, 1994 (originally 1973).
• [15] Kamareddine F, Nederpelt R. A Useful lambda-Notation. Theor. Comput. Sci., 1996. 155(1):85-109. doi:10.1016/0304-3975(95)00101-8.
• [16] Bertot Y, Cast´eran P. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. ISBN:978-3-642-05880-6. doi:10.1007/978-3-662-07964-5.
• [17] Barendregt HP. Lambda calculi with types. In: Abramski S, Gabbai D, Maiboum T (eds.), Handbook of Logic in Computer Science, pp. 117-309. Oxford University Press, Oxford, 1992.
• [18] Coquand T, Huet GP. Constructions: A Higher Order Proof System for Mechanizing Mathematics. In: Buchberger B (ed.), EUROCAL ’85, European Conference on Computer Algebra, Linz, Austria, April 1-3, 1985, Proceedings Volume 1: Invited Lectures, volume 203 of Lecture Notes in Computer Science. Springer, 1985 pp. 151-184. doi:10.1007/3-540-15983-5 13.
• [19] Barendregt HP, Geuvers JH. Proof-Assistants Using Dependent Type Systems. In: Robinson JA, Voronkov A (eds.), Handbook of Automated Reasoning (in 2 volumes), pp. 1149-1238. Elsevier and MIT Press, 2001. doi:10.1016/b978-044450813-3/50020-5.
• [20] Geuvers JH. Proof assistants: history, ideas and future. Sadhana Journal, 2009. 34(1):3-25. [21] Wiedijk F. The Seventeen Provers of the World, Foreword by Dana S. Scott, volume 3600 of Lecture Notes in Computer Science. Springer, 2006. doi:10.1007/11542384 1.
• [22] Naumowicz A, Kornilowicz A. A Brief Overview of Mizar. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science. Springer, 2009 pp. 67-72. doi:10.1007/978-3-642-03359-9 5.
• [23] Gordon M, Melham T. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
• [24] Gordon M. From LCF to HOL: a short history. In: Plotkin GD, Stirling C, Tofte M (eds.), Proof, Language, and Interaction, Essays in Honour of Robin Milner. The MIT Press, 2000 pp. 169-186.
• [25] Church A. A formulation of the simple theory of types. Journal of Symbolic Logic, 1940. 5:56-69.
• [26] Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. ISBN 3-540-43376-7. doi:10.1007/3-540-45949-9.
• [27] de Moura L, Ullrich S. The Lean 4 Theorem Prover and Programming Language. In: Platzer A, Sutcliffe G (eds.), CADE 28, 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science. Springer, 2021 pp. 625-635. doi:10.1007/978-3-030-79876-5 37.
• [28] Bove A, Dybjer P, Norell U. A Brief Overview of Agda – A Functional Language with Dependent Types. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science. Springer, 2009 pp. 73-78. doi:10.1007/978-3-642-03359-9 6.
• [29] Nordström B, Peterson K, Smith JM. Programming in Martin-Löf’s Type Theory : an introduction. Oxford Science Publications, 1990.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)