问题
Isabelle/HOL验证器的核心算法是什么？
我想找到类似于Scheme元循环求值器的东西。
澄清
我只对验证器感兴趣，不关心自动定理证明的策略。
背景
我想从头开始实现一个简单的证明验证器（仅出于教育目的，不用于生产）。
我想了解Isabelle/HOL的核心验证器算法。 我不关心用于自动定理证明的策略/代码。
我怀疑核心验证器算法非常简单（而且优雅）。 但是，我找不到它。
谢谢！
2个回答
11
Isabelle是证明检查器“LCF家族”的成员，这意味着您有一个特殊的模块——推理内核——其中所有推理都通过以产生抽象数据类型thm的值。这有点像操作系统内核处理系统调用。通过这种方式产生的一切都是“正确构造”的，相对于内核实现的正确性而言。由于证明器（Standard ML）的编程语言环境具有非常强的静态类型正确性属性，推理内核的构造正确性可以延伸到证明助手实现的其余部分，这可能非常庞大。
因此，原则上您有一个相对较小的“可信内核”部分和一个真正庞大的“应用用户空间”。特别是，Isabelle/HOL的大部分实际上是Isabelle用户区中的库理论和附加工具（主要在SML中）。
在Isabelle中，内核基础设施相当复杂，但与系统的其余部分相比仍然非常小。实际上，内核被分为“微内核”（
如果你想了解更多关于LCF风格证明器的信息，我建议你也看一下HOL-Light，它可能是LCF家族中最小的实际系统，实际意义上人们已经用它做了大型应用程序。 HOL-Light有一个巨大的优势，即其实现可以很容易地理解，但这种极简主义也有一些缺点：它不能完全保护用户免受在其ML环境中进行无意义操作的影响，该环境使用的是OCaml而不是SML。由于各种技术原因，OCaml默认情况下不像Standard ML那样“安全”。
因此，原则上您有一个相对较小的“可信内核”部分和一个真正庞大的“应用用户空间”。特别是，Isabelle/HOL的大部分实际上是Isabelle用户区中的库理论和附加工具（主要在SML中）。
在Isabelle中，内核基础设施相当复杂，但与系统的其余部分相比仍然非常小。实际上，内核被分为“微内核”（
Thm模块）和“纳米内核”（Context模块）。Thm以Milner的LCF方法为基础生成thm值，而Context则负责任何结果的theory证书，以及本地推理的证明上下文（尤其是在Isar证明语言中）。如果你想了解更多关于LCF风格证明器的信息，我建议你也看一下HOL-Light，它可能是LCF家族中最小的实际系统，实际意义上人们已经用它做了大型应用程序。 HOL-Light有一个巨大的优势，即其实现可以很容易地理解，但这种极简主义也有一些缺点：它不能完全保护用户免受在其ML环境中进行无意义操作的影响，该环境使用的是OCaml而不是SML。由于各种技术原因，OCaml默认情况下不像Standard ML那样“安全”。
- Makarius
2
2
如果您解压Isabelle源代码，例如：
http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
您会在其中找到核心定义。src/Pure/thm.ML
"而且，您想要解决的问题已经有一个项目了：" 后来添加的内容：另一个更严肃的项目是- Gergely
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接
thm以datatype thm = Thm of ...的形式定义，类型构造函数Thm在Thm模块之外是不可见的。因此，只能通过调用返回类型为thm的Thm模块的函数来产生thm类型的值。 - undefined