Towards Self-verification of HOL Light
Towards Self-verification of HOL Light
复制标题
DOI：
10.1007/11814771_17
复制
发表时间：
2006-08
影响因子：
0.9
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
HOL Light证明器基于一个逻辑内核，该内核由大约400行主要功能的OCaml组成，其完整的形式化验证似乎是非常可行的。我们想要正式验证（i）抽象HOL逻辑确实是正确的，以及（ii）OCaml代码确实正确地实现了这个逻辑。我们已经完成了一个不完美的，但相当详细的模型的基本HOL轻核心，没有定义的机制进行了全面的验证，这种验证是完全相对于HOL轻本身的集合论语义。我们将适当地解释为什么明显的逻辑和实际困难并没有使这一方法无效，尽管乍一看它似乎是不可能的或无用的。扩展到包括定义机制似乎足够简单，到目前为止，结果减轻了我们的大部分实际担忧。
The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional OCaml, whose complete formal verification seems to be quite feasible. We would like to formally verify (i) that the abstract HOL logic is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a full verification of an imperfect but quite detailed model of the basic HOL Light core, without definitional mechanisms, and this verification is entirely conducted with respect to a set-theoretic semantics within HOL Light itself. We will duly explain why the obvious logical and pragmatic difficulties do not vitiate this approach, even though it looks impossible or useless at first sight. Extension to include definitional mechanisms seems straightforward enough, and the results so far allay most of our practical worries.