The Wayback Machine - https://web.archive.org/web/20221028225022/https://baike.sogou.com/kexue/d10220.htm

高阶逻辑

编辑

HOL（高阶逻辑）表示一系列使用相似（高阶）逻辑和实现策略的交互式定理证明系统。这个系列中的系统遵循LCF方法，因为它们在一些编程语言中被实现为库。该库实现了一种已证明定理的抽象数据类型，因此这种类型的新对象只能使用库中对应于高阶逻辑推理规则的函数来创建。只要这些函数得到正确实现，系统中证明的所有定理都必须有效。这样，一个大系统可以建立在一个小的可信内核之上。

HOL家族的系统使用ML语言或其后继语言。ML语言最初是与LCF一起开发的，目的是为定理证明系统提供元语言；事实上，这个名字代表“元语言”。

1 底层逻辑编辑

HOL系统使用经典高阶逻辑的变体，这些变体具有简单的公理基础，几乎没有公理，语义也很好理解。[1]HOL谚语中使用的逻辑与Isabelle/[HOL密切相关[2] ，是Isabelle最广泛使用的逻辑。

2 HOL家庭成员编辑

有四个HOL系统（基本上共享相同的逻辑）仍在维护和开发中。

  • 第一，HOL4源自HOL88系统，这是由迈克·戈登领导的最初HOL实施工作的顶峰。HOL88包含它自己的ML语言实现，而ML语言实现又是在公共Lisp之上实现的。HOL88 （HOL90、hol98和HOL4）之后的实现都使用标准ML语言作为实现语言。hol98系统与标准ML的Moscow ML语言实施绑定；HOL4可以用Moscow ML语言或Poly/ML语言制造。在这四个系统中，只有HOL4得到维护和开发。所有系统都带有大型定理证明代码库。这些系统在非常简单的核心代码之上实现了额外的自动化。HOL4是BSD许可的。[3]
  • 第二个当前实施是HOL Light。这开始于HOL的实验性“极简主义”版本。尽管它后来发展成为另一种主流的HOL变体，但它的逻辑基础仍然异常简单。HOL Light过去是在Caml Light中实现的，但现在使用OCaml。根据新的BSD许可证，HOL Light可以使用。[4]
  • 第三个当前实现是 ProofPower，它是一个工具集合，旨在为使用Z符号进行形式规范提供特殊支持。6种工具中有5种是GNU GPL v2许可的。第六个（PPDaz）拥有专有许可证。[5]
  • 第四个是 HOL Zero，一个关注可信度的极简实现。HOL Zero是GNU GPL 3+授权的。[6]

虽然HOL是Isabelle的前身，但各种HOL衍生产品如HOL4和HOL Light仍然活跃并在使用中。

3 选定的形式验证发展编辑

CakeML[7]项目为ML开发了一个经过形式验证的编译器。以前，HOL曾开发过一个在ARM、x86和PowerPC上运行的经过形式验证的LISP实现。[8]

HOL还被用来开发x86多处理器的形式语义，[9]以及Power ISA和ARM体系结构的机器代码语义。[10]

参考文献

  • [1]

    ^Andrews, Peter B (2002). An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series. 27 (Second ed.). Dordrecht: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7..

  • [2]

    ^Tobias Nipkow; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1..

  • [3]

    ^https://web.archive.org/web/20221028225022/http://hol-theorem-prover.org/.

  • [4]

    ^https://web.archive.org/web/20221028225022/http://www.cl.cam.ac.uk/users/jrh/hol-light/.

  • [5]

    ^https://web.archive.org/web/20221028225022/http://www.lemma-one.com/ProofPower/getting/.

  • [6]

    ^See LICENSE file in the tarball..

  • [7]

    ^https://web.archive.org/web/20221028225022/https://cakeml.org/.

  • [8]

    ^Magnus O. Myreen; Michael J. C. Gordon. Verified LISP Implementations on ARM, x86 and PowerPC (PDF). TPHOLs 2009. pp. 359–374..

  • [9]

    ^Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). "x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors" (PDF). Communications of the ACM. 53 (7): 89–97..

  • [10]

    ^Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009:. pp. 13–24..

阅读 127
版本记录

  • 暂无