证明助手如何实施？

Question

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

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

对于编译器，我也提出了类似的问题：https : //softwareengineering.stackexchange.com/questions/165543/how-to-write-a-very-basic-compiler

我的担心是一样的，但对于校对系统。

Answer 1

我几乎没有对此事的专家（我是这些系统的唯一用户，我不担心太多关于他们的内部），这可能只是一个模糊的部分答案，但两个主要的方法，我知道的是：

• 使用Curry-Howard同构的依赖类型系统（例如Coq，Lean，Agda）。语句只是类型，证明是具有该类型的术语，因此检查证明的有效性本质上只是对术语进行类型检查的一种特殊情况。我不想过多地谈论这种方法，因为我对此不太了解，恐怕会出错。温特豪德（ThéWinterhalter）在上面的评论中链接了一些内容，可能会提供有关此方法的更多上下文。
• LCF样式定理得到证明（例如Isabelle，HOL Light，HOL 4）。这里的一个定理（大致而言）是thm实现语言中type的不透明值。只有相对较小的“证明内核”才能创建这些thm值，并且系统的所有其他部分都与该证明内核交互。内核提供了一个由各种小功能组成的接口，这些接口实现了小的推理步骤，例如惯性定理（如果有一个定理A ? B和一个定理A，就可以得到该定理B）或？-引入（如果有P x一个固定变量的定理x，你可以得到定理?x. P x）等。内核还提供了用于定义新常量的接口。原则上，只要您可以相信这些函数能够忠实地实现基础逻辑的基本推理步骤，就可以相信thm可以产生的任何值确实对应于逻辑中的一个定理。对于LCF风格的证明者，要回答实际证明的内容要困难一些，因为它们通常不建立证明术语（例如Isabelle拥有它们，但是默认情况下它们被禁用并且未广泛使用）。我认为可以说内核原语如何被调用的历史构成了证明，并且，如果要记录下来，原则上可以在另一系统中重放和检查。

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

所有这些不同的系统都在系统的哪些部分位于内核中以及哪些部分不在内核中进行了各种折衷。总的来说，我认为可以说与基于LCF的系统相比，从属类型的系统往往具有更大的内核（例如，HOL Light具有特别小的和简单的内核）。

我相信还有其他一些系统不适合这两个类别（例如Mizar，ACL2，PVS，Metamath，NuPRL），但我对这些系统的实现方式一无所知。