Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
HOL Light
[go: Go Back, main page]

The HOL Light theorem prover

Written by John Harrison drawing on the work of
Mike Gordon Tom Melham Robin Milner Larry Paulson Konrad Slind
and many other HOL and LCF researchers

HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.

HOL Light is now a Google Code project so you can get the sources from the Google Code repository. You can browse individual source files online, or check out all the code using subversion. For example, the following command will copy all the code from the trunk of the Google Code repository into a new directory hol_light: 

svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
HOL Light is written in Objective CAML (OCaml), and it should work with any reasonably recent version. To build with OCaml 3.10 and later you will also need to install camlp5, version 5.07 or higher. See the README file in the distribution for detailed installation instructions.

For those who prefer to download a packaged version directly instead of using subversion, a snapshot from 10th January 2010 is available as a gzipped tar file or as a zip file. The last numbered release, now quite old, is 2.20, which you can get here. (Note that 2.20 doesn't work under OCaml >= 3.10, owing to changes to camlp4. If you really want to use HOL Light with these versions of OCaml, use one of the more recent versions listed above.) Experimental Linux binaries for version 2.20 are also now available, created using CryoPID. NB: I'm not sure how portable these are across Linux versions; better to build from source if you can. The files are hol (core system), hol.sosa (preloaded with analysis and sum-of-squares tools), hol.multivariate (preloaded with multivariate analysis) and hol.card (preloaded with cardinal arithmetic). Note that although these work as standalone executables, if you are planning to work much with the system, you'll probably still want to download the HOL sources to give access to additional library directories and to the help files. For example, if you download the HOL Light source tree to "/home/myself/hol_light", you might start a HOL Light session with the following so that HOL Light can find all the files (# is the OCaml prompt): 

   # hol_dir := "/home/myself/hol_light";;
   val it : unit = ()
   # load_path := ["."; !hol_dir];;
   val it : unit = ()
The following lists some available documentation and resources:

Here are some applications of HOL Light: HOL Light is free open source software. It comes with no warranty of any kind (see the LICENCE file in the distribution), and no guarantee of maintainance. However, please feel free to send any comments or questions to the author at .
Last updated by John Harrison on 16th October 2011.