coq - 证明助手是如何实现的？

Question

证明助手的主要功能是什么？

我只是想知道证明检查的内部逻辑。例如，关于此类助手的图形用户界面的主题我不感兴趣。

编译器也问了一个与我类似的问题:
https://softwareengineering.stackexchange.com/questions/165543/how-to-write-a-very-basic-compiler

我的担忧是一样的，但对于证明检查系统。

Answer 1

我几乎不是这方面的专家(我只是这些系统的用户；我不太担心它们的内部结构)，这可能只是一个模糊的部分答案，但我知道的两种主要方法是:

使用 Curry-Howard 同构的依赖类型系统(例如 Coq、Lean、Agda)。语句只是类型，而证明是具有该类型的术语，因此检查证明的有效性本质上只是类型检查术语的一种特殊情况。这个方法我不想多说，因为我对它了解的不多，怕会出错。 Théo Winterhalter 在上面的评论中链接了一些内容，可能会为这种方法提供更多背景信息。

LCF 风格的定理证明器(例如 Isabelle、HOL Light、HOL 4)。这里的定理是(粗略地说)类型为 thm 的不透明值。在实现语言中。只有相对较小的“证明内核”才能创建这些 thm值和系统的所有其他部分与这个证明内核交互。内核提供了一个由各种小函数组成的接口(interface)，这些函数实现了小推理步骤，例如前件推理(如果你有一个定理 A ⟹ B 和一个定理 A，你可以得到定理 B)或∀-介绍(如果你有定理 P x 用于固定变量 x ，你可以得到定理 ∀x. P x ) 等。内核还提供了一个定义新常量的接口(interface)。原则上，只要你能相信这些函数忠实地实现了底层逻辑的基本推理步骤，你就可以相信任何 thm您可以产生的值确实对应于您逻辑中的定理。对于 LCF 风格的证明者，实际证明的答案有点难以回答，因为它们通常不构建证明术语(例如，Isabelle 有它们，但默认情况下它们被禁用并且没有被广泛使用)。我认为可以说内核原语被调用的历史构成了证明，如果要记录它，原则上可以在另一个系统中重放和检查。

在这两种情况下，你的想法是你有一个你必须信任的内核(前一种情况下的类型检查器和后一种情况下的推理内核)，然后你有一个围绕此的附加程序的大型生态系统，以提供更多便利层.但是，由于它们必须与内核交互才能实际产生定理，因此您不必信任该代码。

所有这些不同的系统对于系统的哪些部分在内核中以及哪些部分不在内核中都有不同的权衡。总的来说，我认为可以公平地说，依赖类型系统的内核往往比基于 LCF 的系统大得多(例如，HOL Light 的内核特别小且简单)。

还有其他一些系统我认为不属于这两个类别(例如 Mizar、ACL2、PVS、Metamath、NuPRL)，但我对这些是如何实现的一无所知。