HOL theorem prover

This paragraph should be moved to the LCF article when it's written... HOL follows 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.

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. 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://lal.cs.byu.edu/lal/hol-documentation.

HOL is a succesor of LCF theorem prover.

http://sourceforge.net/projects/hol/

Among the successors of HOL is Isabelle theorem prover.