10.46298/fi-2022-9343
https://fi.episciences.org/9343
Geuvers, Herman
Herman
Geuvers
Nederpelt, Rob
Rob
Nederpelt
Characteristics of de Bruijn's early proof checker Automath
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, which was one
of the first widely used interactive theorem provers and forms the basis for
the widely used Coq system. The original syntax of Automath 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 {\lambda}D, a
direct extension of CC with definitions.
episciences.org
Computer Science - Logic in Computer Science
Mathematics - Logic
68V15, 03B35
F.4
2022-04-28
2022-07-07
2022-07-07
eng
journal article
arXiv:2203.01173
10.48550/arXiv.2203.01173
1875-8681
https://fi.episciences.org/9343/pdf
VoR
application/pdf
Fundamenta Informaticae
Volume 185, Issue 4
Researchers
Students