HOL theorem prover

From Wikipedia, the free encyclopedia

The various HOL (which stands for Higher Order Logic) systems are a family of interactive theorem proving systems sharing similar logics and implementation strategies. All of these systems follow the LCF approach. In this approach, the system is actually implemented as a library in some programming language. This library implements an abstract data type of proven theorems; it is impossible to create a new object of this type without using the functions in the library. The functions in the library correspond to inference rules in the HOL 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. This language 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".

There are three 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. HOL4 and hol98 are tied to the Moscow ML implementation of Standard 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.

For more information about HOL, see http://hol.sourceforge.net/.

HOL is a successor of the LCF theorem prover. Among the successors of HOL is the Isabelle theorem prover.