时间戳

首页 > 解决方案 > 证明助手是如何实现的？

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

问题描述

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

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

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

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

标签： coqisabelleproof

解决方案

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

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

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

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

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

推荐阅读