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
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.
You can download the sources for the latest version 2.20 here. It should work on pretty much any
platform under most recent versions of Ocaml. (Note that
2.20 doesn't yet work under the very latest OCaml, 3.10, owing to changes to
camlp4. If you really want to use HOL Light with 3.10, use the development
snapshot below. You will also need to install camlp5.) See the README
file in the distribution for detailed installation instructions.
A Development snapshot from 19th February
2008 is available. This is not an official release and may be
buggy, but it should give some idea of what's likely to change in 2.30. It
should build under any reasonably recent OCaml. To build with OCaml 3.10 and
later you will also need to install camlp5 version 5.07.
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:
Formalization of floating-point arithmetic, and the formal verification of
several floating-point algorithms at Intel. See this paper for a quick
summary and more references, and this one for a more
detailed presentation.
The Flyspeck project
to machine-check Tom Hales's
proof of the Kepler conjecture. Tom has already proved the Jordan Curve
Theorem and other relevant results in HOL Light.
Many other mathematical results of varying degrees of difficulty have been
verified in HOL Light. See for example the HOL Light entries on the Formalizing 100 Theorems page.
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 19th February 2008.