Isabelle/HOL验证器的核心算法是什么？
我正在寻找一个计划水平评估员的水平.
我只对Verifier感兴趣,而不是自动定理证明的策略.
我想从头开始实现一个简单的验证验证器(纯粹出于教育原因,而不是用于生产用途.)
我想了解Isabelle/HOL 的核心Verifier算法.我不关心用于自动定理证明的策略/代码.
我怀疑核心Verifier算法非常简单(而且优雅).但是,我找不到它.
谢谢!
Mak*_*ius 10
Isabelle是证明检查器的"LCF系列"的成员,这意味着你有一个特殊的模块---推理内核 - 所有的推论都贯穿其中以产生抽象数据类型的值thm.这有点像操作系统内核处理系统调用.相对于内核实现的正确性,您可以通过这种方式生成的所有内容都是"正确的构造".由于证明器(标准ML)的编程语言环境具有非常强的静态类型正确性属性,因此推理内核的构造的正确性延续到证明助理实现的其余部分,这可能是非常大的.
所以原则上你有一个相对较小的"可信内核"部分和一个非常大的"应用程序用户空间".特别是,大多数Isabelle/HOL实际上是Isabelle用户界中的大量图书馆理论和附加工具(主要是SML).
在Isabelle中,内核基础结构非常复杂,但与系统的其他部分相比仍然非常小.内核实际上层叠成"微内核"(该Thm模块)和"纳米内核"(该Context模块). Thm产生thm在米尔纳的LCF-方法的感测值,以及Context需要照顾theorycertficates对您产生任何结果,以及证明对上下文推理的地方(特别是在伊萨尔证明语言).
如果你想了解更多关于LCF风格的证据,我建议你再看一下HOL-Light,这可能是LCF系列中最小的现实系统,从某种意义上讲,人们已经用它做了大量应用.HOL-Light具有很大的优势,它的实现可以很容易理解,但这种极简主义也有一些不利之处:它不能完全保护用户在其ML环境中无意义,这是OCaml而不是SML.由于各种技术原因,OCaml默认情况下不像标准ML那样"安全".
如果您解压 Isabelle 源代码，例如
http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
你会发现核心定义
src/Pure/thm.ML
而且，您已经有一个想要解决的项目：
http://www.proof-technologies.com/holzero/
稍后添加：另一个更严肃的项目是
https://team.inria.fr/parsifal/proofcert/