证明助手是如何实现的？答案

【问题标题】：How proof assistants are implemented?证明助手是如何实现的？
【发布时间】：2019-11-06 08:04:44
【问题描述】：

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

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

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

我的关注点是一样的，但对于证明检查系统。

【问题讨论】：

这有点宽泛，但你可以看看这篇不错的博文：例如math.andrej.com/2018/08/25/…。
对不起。这可能是因为我是这个主题的新手。如果您对如何改进我的问题有任何建议，请告诉我。非常感谢您的帮助。
另外，您是否包括用户界面或此类东西，或者您只是想知道证明助手的内部逻辑？如果你想了解 coq，还有 metacoq 项目，它指定了 coq 的（一个子集）。
非常感谢！其实我只是想了解内部逻辑。

标签： coq isabelle proof

【解决方案1】：

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

使用 Curry-Howard 同构的依赖类型系统（例如 Coq、Lean、Agda）。语句只是类型，而证明是具有该类型的术语，因此检查证明的有效性本质上只是类型检查术语的一种特殊情况。这种方法我不想多说，因为我对它了解的不多，怕会出错。 Théo Winterhalter 链接了上述 cmets 中的一些内容，这些内容可能会为这种方法提供更多背景信息。
LCF 式定理证明器（例如 Isabelle、HOL Light、HOL 4）。这里的定理（粗略地说）是实现语言中thm 类型的不透明值。只有相对较小的“证明内核”可以创建这些thm 值，并且系统的所有其他部分都与这个证明内核交互。内核提供了一个由各种小函数组成的接口，这些函数实现了小推理步骤，例如 modus ponens（如果你有定理A ⟹ B 和定理A，你可以得到定理B ) 或∀-介绍（如果你有定理P x 用于固定变量x，你可以得到定理∀x. P x）等等。内核还提供了一个定义新常量的接口。原则上，只要您可以相信这些函数忠实地实现了底层逻辑的基本推理步骤，您就可以相信您可以产生的任何thm 值确实对应于您的逻辑中的一个定理。对于 LCF 风格的证明者，实际证明的答案有点难以回答，因为它们通常不构建证明术语（例如，Isabelle 有它们，但默认情况下它们被禁用并且没有被广泛使用）。我认为可以说内核原语被调用的历史构成了证明，如果要记录它，它可以 - 原则上 - 在另一个系统中重放和检查。李>

在这两种情况下，您的想法是您必须拥有一个必须信任的内核（前一种情况下的类型检查器和后一种情况下的推理内核），然后您有一个庞大的生态系统，其中包含额外的过程来提供更多便利层。但是，由于它们必须与内核交互才能实际产生定理，因此您不必信任该代码。

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

我认为还有其他系统不属于这两个类别（例如 Mizar、ACL2、PVS、Metamath、NuPRL），但我不知道它们是如何实现的。

【讨论】：

【解决方案2】：

对于 LCF、HOL 和 Isabelle，您可以在期刊文章“From LCF to Isabelle/HOL”中找到对您问题的广泛解答。（它是开放访问。）

如文章和 Eberl 的回答中所述，大多数依赖类型的系统（例如 Coq）也是 LCF 风格的定理证明器。一个显着的区别是此类演算包含完整的证明对象，因此 LCF 方法的目标之一——通过不存储证明来节省空间——被放弃了。不过，稳健的目标还是达到了。

【讨论】：