de Bruijn 早期证明检查器 Automath 的特征
计算机科学中的逻辑
2023-06-22 v3 逻辑
摘要
由 N.G. de Bruijn 于 1968 年构想的“数学语言” Automath 是首个实际运行的定理证明器，并已被用于检查大量数学内容样本。其目标与语法思想启发了 Th. Coquand 与 G. Huet 开发构造演算（CC），后者是最早被广泛使用的交互式定理证明器之一，并构成了广泛使用的 Coq 系统的基础。Automath 的原始语法不易掌握。然而，它本质上基于一种类似于构造演算（‘CC’）的推导系统。尽管类型论学界对 Automath 多有引用，Automath 语法与 CC 之间的关系尚未被充分描述。本文聚焦于 Automath 语法的背景与若干不常见方面。我们阐明了“通用” Automath 系统的基本方面，该系统封装了最常见的 Automath 版本。我们以现代语法框架呈现此通用 Automath 系统。所得系统使用了 λD，即带定义项的 CC 的直接扩展。
引用
@article{arxiv.2203.01173,
title = {Characteristics of de Bruijn's early proof checker Automath},
author = {Herman Geuvers and Rob Nederpelt},
journal= {arXiv preprint arXiv:2203.01173},
year = {2023}
}