The HOL theorem prover

Please contact Jonathan Bowen if you know of relevant on-line information not included here.

This document contains some pointers to information on the

HOL mechanical theorem proving system, based on Higher Order Logic, available around the world on the World Wide Web (WWW or W3), a global hypermedia system providing worldwide information.

The following on-line information is available:

The HOL System. Information provided by the Automated Reasoning Group at the University of Cambridge Computer Laboratory, UK. See also FTP archive.
HOL 4 and Project information - HOL theorem-proving system from SourceForge.
HOL documentation at Brigham Young University (second sourced in the UK).
The sources for the HOL system (with an index) at the University of Cambridge Computer Laboratory (second sourced in the US).
Archive material including papers and contributed software for HOL (with a README file) are available.
Release Note for HOL from the Automated Reasoning Group at Cambridge.
The info-hol electronic mailing list enables discussion on topics concerning HOL and includes annnouncements of HOL meetings. Contact info-hol-request@lal.cs.byu.edu to be added to the list. The archives are searchable and there is a list of subscribers.
Conferences related to the HOL System. See TPHOLs'98: International Conference on Theorem Proving in Higher Order Logics, Canberra, Australia, 21 September - 2 October 1998.
The HOL2000 initiative is trying to put together a design for the next generation of HOL-like theorem proving environments. To join the discussion list, email hol2000-request@lal.cs.byu.edu.
Some support for the Z notation is available as documented in the paper Z and HOL. The source files for various Z specifications in HOL are available.
ProofPower is a commercial tool, developed and marketed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z.
HOL-Z tool. A shallow embedding of the Z notation in the higher-order logic theorem prover Isabelle, similar to that of the HOL system. Also mirrored here and here.
Information on the HOL Theorem Prover from the Formal Methods and Theory Group at Glasgow.
A good introductory book is Introduction to HOL: A theorem proving environment for higher order logic, edited by M.J.C. Gordon and T.F. Melham, 1993. ISBN: 0 521 44189 7 See also:
- Other information on books, especially concerning hardware verification.
- Publisher's information from Cambridge University Press. ISBN: 0 521 44189 7.
- A book review of ``An introduction to HOL'' by Graham Hutton.
- Order from your bookstore (e.g., from Amazon USA or Amazon UK).
Higher Order Logic theorem provers pointers from Yahoo.
CHOL distribution from INRIA, an attempt to privide a better user interface for HOL using the Centaur system.
Higher Order Logic Theorem Proving and its Applications special issue of The Computer Journal by Tom Melham.
HOL Light by John Harrison.

See also PVS, another newer theorem proving tool based on higher order logic.

Last updated by Jonathan Bowen, 17 February 2005.
Further information for possible inclusion is welcome.

Part of the LSBU Museophile archive.