HOL 4	Kananaskis 4
	Easier to use: easy installation, bugs fixed! Cool examples: ARM6, λ-calculus, PSL, ACL2 New libraries: BDDs, SAT, model-checking New documentation: Extended Description, DPLL example, ...
|  Release notes |  Documentation |  FAQ |  Online reference |  Emacs mode |  Installing from Sources  |  Windows installer |  HOL@S/F |  Anon SVN |

What is HOL 4?

HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

Other HOLs are described elsewhere.

Downloads

• Sources (and also, via Subversion)
• Windows installer

History

During the last 20 years there have been several widely used versions of the HOL system:

1. HOL88 from Cambridge;
2. HOL90 from Calgary and Bell Labs;
3. HOL98 from Cambridge, Glasgow and Utah.

HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL. It was originally developed by ICL, but is now freely available from Lemma 1. All the HOL systems use Robin Milner's LCF approach.

How easy is it to learn?

Starting from scratch, it takes on average about a month to become comfortable using HOL. Many people learn the system from the free tutorial, others take courses that are offered from time to time.

Support and licencing

HOL 4 is an open source project with a BSD-style licence that allows its free use in commercial products. New developers are welcome.

Support and information is available online:

• the hol-info mailing list is for discussion, questions and announcements related to the HOL System (HOL4 and HOL Light discussions are both welcome)
  • [hol-info@lists.sourceforge.net | subscribe | archives]
• Bug reports: click here.

HOL is developed by researchers at (among other places):