Question
Isabelle/HOL验证器的核心算法是什么?
我正在寻找方案元循环评估器级别的东西。
澄清
我只对Verifier,而不是自动定理证明的策略。
Context
我想从头开始实现一个简单的证明验证器(纯粹出于教育原因,而不是用于生产用途。)
我想了解核心VerifierIsabelle/HOL 的算法。我不关心用于自动定理证明的策略/代码。
我怀疑核心Verifier算法非常简单(而且优雅)。但是,我找不到它。
Thanks!
Isabelle 是证明检查器“LCF 系列”的成员,这意味着您有一个特殊的模块——推理内核——所有推理都会在其中运行以生成抽象数据类型的值thm
。这有点像操作系统内核处理系统调用。相对于内核实现的正确性,您可以通过这种方式生成的所有内容都是“构造正确的”。由于证明者(标准 ML)的编程语言环境具有非常强的静态类型正确性属性,因此推理内核的构造正确性会延续到证明助手实现的其余部分,这可能非常巨大。
因此原则上你有一个相对较小的“可信内核”部分和一个非常大的“应用程序用户空间”。特别是,大部分 Isabelle/HOL 实际上是 Isabelle 用户空间中库理论和附加工具(主要是 SML)的大集合。
在 Isabelle 中,内核基础设施相当复杂,但与系统的其他部分相比仍然非常小。内核实际上分层为“微内核”(the Thm module)和“纳米内核”(the Context module). Thm
产生thm
米尔纳 LCF 方法意义上的值,以及Context
照顾theory
您产生的任何结果的证书,以及本地推理的证明上下文(特别是 Isar 证明语言)。
如果您想了解有关 LCF 式证明器的更多信息,我建议您还可以查看HOL-光这可能是 LCF 系列中最小的现实系统,从人们已经用它完成大型应用的意义上来说,它是现实的。 HOL-Light 的一大优点是它的实现很容易理解,但这种极简主义也有一些缺点:它不能完全保护用户在其 ML 环境(即 OCaml 而不是 SML)中做无意义的事情。由于各种技术原因,OCaml 默认情况下并不像标准 ML 那样“安全”。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)