请输入您要查询的百科知识：

　

词条 HOL (proof assistant)
释义

  1. Underlying logic

  2. Members of HOL family of provers

  3. Selected formal proof developments

  4. References

  5. External links

{{Infobox programming language
| name = HOL
| designer = Michael J C Gordon
| license = Modified (3-clause) BSD licence
| website = {{url|hol-theorem-prover.org}}
| file_ext = .sml
}}

HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using

similar (higher-order) logics and implementation strategies.

Systems in this family follow the LCF approach as they are implemented as a library in some programming language.

This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. In this way, a large system can be built on top of a small trusted kernel.

Systems in the HOL family use the ML programming language or its successors. ML was originally developed along with LCF to serve the purpose of a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".

Underlying logic

HOL systems use variants of classical Higher-order logic, which has simple axiomatic foundations with few axioms and well-understood semantics.[1]

The logic used in HOL provers is closely related to Isabelle/HOL,[2] the most widely used logic of Isabelle.

Members of HOL family of provers

There are four HOL systems (sharing essentially the same logic) that are still maintained and developed.

  • The first, HOL4 stems from the HOL88 system, which was the culmination of the original HOL implementation effort, led by Mike Gordon. HOL88 included its own ML implementation, which was in turn implemented on top of Common Lisp. The implementations following HOL88 (HOL90, hol98 and HOL4) all used Standard ML as the implementation language. The hol98 system is tied to the Moscow ML implementation of Standard ML; HOL4 can be built with either Moscow ML or Poly/ML. Of these four systems, only HOL4 is being maintained and developed. All come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code. HOL4 is BSD licensed.[3]
  • The second current implementation is HOL Light. This started as an experimental "minimalist" version of HOL. Although it has subsequently grown into another mainstream HOL variant, its logical foundations remain unusually simple. HOL Light used to be implemented in Caml Light, but now uses OCaml. HOL Light is available under the new BSD license.[4]
  • The third current implementation is ProofPower a collection of tools designed to provide special support for working with the Z notation for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.[5]
  • The fourth is HOL Zero, a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed.[6]

Although HOL is a predecessor of Isabelle, various HOL derivatives such as HOL4 and HOL Light remain active and in use.

Selected formal proof developments

CakeML[7] project developed a formally proven compiler for ML (programming language).

Previously, HOL was used to developed a formally proven LISP implementation running on ARM, x86 and PowerPC.[8]

HOL was also used to develop formal semantics for x86 multiprocessors,[9] as well as semantics of machine code for Power ISA and ARM architectures.[10]

References

1. ^{{cite book|last=Andrews|first=Peter B|year=2002|title=An introduction to mathematical logic and type theory: to truth through proof|edition=Second|series=Applied Logic Series|volume=27|isbn=978-1-4020-0763-7|publisher=Kluwer Academic Publishers|location=Dordrecht}}
2. ^{{cite book|author1=Tobias Nipkow|author2=Markus Wenzel|author3=Lawrence C. Paulson|year=2002|title=Isabelle/HOL: A Proof Assistant for Higher-Order Logic|publisher=Springer-Verlag|location=Berlin, Heidelberg|isbn=978-3-540-45949-1}}
3. ^http://hol-theorem-prover.org/
4. ^http://www.cl.cam.ac.uk/users/jrh/hol-light/
5. ^http://www.lemma-one.com/ProofPower/getting/
6. ^See LICENSE file in the tarball.
7. ^https://cakeml.org/
8. ^{{cite conference|author1=Magnus O. Myreen|author2=Michael J. C. Gordon|title=Verified LISP Implementations on ARM, x86 and PowerPC|conference=TPHOLs 2009|pages=359-374|url=https://www.cl.cam.ac.uk/~mom22/tphols09-lisp.pdf}}
9. ^{{cite journal|author1=Peter Sewell|author2=Susmit Sarkar|author3=Scott Owens|author4=Francesco Zappa Nardelli|author5=Magnus O. Myreen|title=x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors|journal=Communications of the ACM|volume=53|issue=7|pages=89-97|year=2010|url=https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf}}
10. ^{{cite conference|author1=Jade Alglave|author2=Anthony C. J. Fox|author3=Samin Ishtiaq|author4=Magnus O. Myreen|author5=Susmit Sarkar|author6=Peter Sewell|author7=Francesco Zappa Nardelli|title=The Semantics of Power and ARM Multiprocessor Machine Code|conference=DAMP 2009:|pages=13-24|url=http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf}}
  • {{cite web

| last = Gordon
| first = Michael J. C.
| authorlink = Michael J. C. Gordon
| year = 1996
| title = From LCF to HOL: a short history
| url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
| accessdate = 2007-10-11 }}

External links

  • HOL4 Project homepage
  • Documents specifying HOL's basic logic
  • The HOL4 Description manual, which includes a specification of the system's logic.
  • Virtual library formal methods information

2 : Proof assistants|Logic in computer science
随便看

　

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。

　

Copyright © 2023 OENC.NET All Rights Reserved
京ICP备2021023879号 更新时间：2024/11/10 11:52:34