HOL theorem prover

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 should be information on the HOL logic here.

There are four separate implementations of HOL. The first, HOL88, is the culmination of the original HOL implementation effort, led by Mike Gordon. It includes its own ML implementation, and is implemented on top of Common Lisp. The second, HOL90, uses Standard ML. The third, HOL98, uses Moscow ML. The current HOL 4 project is based on HOL98 and continues to use Moscow ML.

These three HOL implementations come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code.

The fourth implementation, HOL Light, is much simpler than the others. It uses simpler axioms and inference rules to describe its logic (although the logic is essentially the same as other HOL implementations). It also has fewer libraries of automated tactics. HOL Light is implemented in CAML Light.

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.