HOL theorem prover
Encyclopedia
HOL denotes a family of interactive theorem proving
systems sharing
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 theorem
s 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".
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.
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.
The third current implementation is ProofPower, originally a commercial system, designed to provide special support for working with the Z notation
for formal specification. Like all the other implementations, ProofPower is now an Open source
project.
The fourth is HOL Zero, a minimalist
implementation focused on trustworthiness.
HOL is a predecessor of Isabelle.
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
systems sharing
similar (higher-order)
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
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
Abstract data type
In computing, an abstract data type is a mathematical model for a certain class of data structures that have similar behavior; or for certain data types of one or more programming languages that have similar semantics...
of proven theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s 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
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
. 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
ML programming language
ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...
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".
Members
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
Common Lisp
Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
.
The implementations following HOL88 (HOL90, hol98 and HOL4) all used Standard ML
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
as the implementation language. The hol98 system is tied to the Moscow ML
Moscow ML
Moscow ML is an implementation of Standard ML.The codebase is derived from Caml Light.The latest release is 2.01. Supported platforms include Unix, Windows, Mac OS and .NET.- External links :*...
implementation of Standard ML
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
; HOL4 can be built with either Moscow ML
Moscow ML
Moscow ML is an implementation of Standard ML.The codebase is derived from Caml Light.The latest release is 2.01. Supported platforms include Unix, Windows, Mac OS and .NET.- External links :*...
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.
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.
The third current implementation is ProofPower, originally a commercial system, designed to provide special support for working with the Z notation
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
for formal specification. Like all the other implementations, ProofPower is now an Open source
Open source
The term open source describes practices in production and development that promote access to the end product's source materials. Some consider open source a philosophy, others consider it a pragmatic methodology...
project.
The fourth is HOL Zero, a minimalist
implementation focused on trustworthiness.
HOL is a predecessor of Isabelle.
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