论文标题
De Bruijn的早期证明检查器Automath的特征
Characteristics of de Bruijn's early proof checker Automath
论文作者
论文摘要
N.G.构思的“数学语言”自动De Bruijn于1968年是第一个实际工作的定理供体，用于检查许多数学内容的标本。它的目标和句法思想启发了。 Coquand and G. Huet开发了构造的计算CC，CC是首批广泛使用的交互式定理掠夺者之一，并构成了广泛使用的COQ系统的基础。 Automath的原始语法并不容易掌握。但是，它本质上是基于类似于构造（`cc'）的衍生系统。尽管类型理论社区中有很多参考文献，但尚未充分描述自动脉语语法与CC之间的关系。在本文中，我们专注于Automath语法的背景和一些罕见的方面。我们揭示了“通用”汽车系统的基本方面，并封装了最常见的自动变速箱。我们在现代的句法框架中介绍了这个通用的自动变量系统。获得的系统利用λd，λd是具有定义的CC的直接扩展。
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 λD, a direct extension of CC with definitions.
