问题
Isabelle/HOL验证器的核心算法是什么？
我正在寻找计划元循环评估器级别的东西。
澄清
我只对Verifier感兴趣，而不是自动定理证明的策略。
语境
我想从头开始实现一个简单的证明验证器（纯粹是出于教育原因，而不是用于生产用途。）
我想了解 Isabelle/HOL 的核心Verifier算法。我不关心用于自动定理证明的策略/代码。
我怀疑核心验证器算法非常简单（而且优雅）。但是，我找不到它。
谢谢！
问问题
639 次
2 回答
11
Isabelle 是“LCF 系列”证明检查器的成员，这意味着您有一个特殊的模块——推理内核——所有推理都在其中运行以产生抽象数据类型的值thm。这有点像操作系统内核处理系统调用。相对于内核实现的正确性，您可以通过这种方式生成的所有内容都是“构造正确的”。由于证明者的编程语言环境（标准 ML）具有非常强的静态类型正确性属性，推理内核的构造正确性会延续到证明助手实现的其余部分，这可能是非常巨大的。
所以原则上你有一个相对较小的“可信内核”部分和一个非常大的“应用程序用户空间”。特别是，Isabelle/HOL 的大部分内容实际上是 Isabelle 用户空间中大量的图书馆理论和附加工具（主要是 SML）的集合。
在 Isabelle 中，内核基础结构非常复杂，但与系统的其余部分相比仍然非常小。内核实际上分为“微内核”（模块Thm）和“纳米内核”（模块Context）。 Thm产生thmMilner 的 LCF 方法意义上的值，并Context处理theory您产生的任何结果的证书，以及本地推理的证明上下文（特别是在 Isar 证明语言中）。
如果你想了解更多关于 LCF 风格的证明者，我建议你也看看HOL-Light，它可能是 LCF 系列中最小的现实系统，在人们用它完成大型应用的意义上是现实的。HOL-Light 最大的优点是它的实现可以很容易理解，但是这种极简主义也有一些缺点：它并没有完全保护用户在它的 ML 环境中做无意义的事情，它是 OCaml 而不是 SML。由于各种技术原因，OCaml 默认情况下不如标准 ML 那样“安全”。
于 2013-02-28T21:05:17.513 回答
2
如果你解开 Isabelle 的来源，例如
http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
您将在中找到核心定义
src/Pure/thm.ML
而且，您已经有这样一个项目要处理：
http://www.proof-technologies.com/holzero/
后来补充：另一个更严肃的项目是
于 2013-02-28T16:54:11.237 回答