欧几里得《几何原本》的证明检验
计算机科学中的逻辑
2018-10-22 v2
摘要
我们使用计算机证明检验方法验证了我们对欧几里得《几何原本》第一卷中命题证明的正确性。我们使用的公理尽可能接近欧几里得的公理，采用的语言与 Tarski 形式化几何中使用的语言密切相关。我们使用的证明尽可能接近欧几里得给出的证明，但填补了欧几里得的遗漏并纠正了错误。欧几里得《几何原本》第一卷有 48 个命题，我们证明了 235 个定理。这些额外的定理部分是“第零卷”（Book Zero），即具有非常基本性质的预备知识；部分是欧几里得省略但隐式使用的命题；部分是我们发现填补欧几里得遗漏所必需的高级定理；还有部分仅是欧几里得命题的变体。我们用与欧几里得逻辑相对应的一阶逻辑的一个简单片段编写了这些证明，使用定制的软件工具对其进行调试，然后在广受认可且可信的证明检查器 HOL Light 和 Coq 中对其进行了检验。
引用
@article{arxiv.1710.00787,
title = {Proof-checking Euclid},
author = {Michael Beeson and Julien Narboux and Freek Wiedijk},
journal= {arXiv preprint arXiv:1710.00787},
year = {2018}
}
备注
53 pages