在 Tarski 几何中寻找证明

我们报告了一个使用定理证明器寻找 Tarski 几何定理证明的项目。这些定理从介于性的基本性质开始，经过 Gupta 的几个著名定理的推导，最后以从 Tarski 公理推导 Hilbert 1899 年的几何公理结束。它们包括 Quaife 留下的四个未解决的挑战问题，他在二十年前在 Tarski 几何中找到了一些 \Otter 证明（解决了 Wos 1998 年著作中提出的挑战）。该集合中共有 212 个定理。我们能够找到所有这些定理的 \Otter 证明。我们开发了一种自动化准备和检查这些定理输入文件的方法，以确保没有人为错误破坏体现在两百个输入文件和证明中的整个理论的形式化发展。我们区分了完全机械找到的证明（不参考书籍证明的步骤）和通过涉及人类了解书籍证明步骤的某种技术构建的证明。粗略地说，长度为 40--100 步的证明对人类来说是困难的练习，而 100-250 步的证明属于博士论文或出版物。我们集合中的 29 个证明长于 40 步，十个长于 90 步。在 183 个具有“短”证明（40 个或更少推导步骤）的定理中，除了 26 个之外，我们都能够完全机械地推导出来。我们使用一种需要在开始时参考书籍证明的方法，找到了其余定理以及 29 个“困难”定理的证明。我们的“子公式策略”使我们能够完全机械地证明 29 个困难定理中的四个。这些是博士级别的证明，长度高达 108 步。