**The HOL theorem prover**

Please edit this page or contact Jonathan Bowen if you know of relevant online 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).

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 announcements 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: - 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, 24 March 2009.

Further information for possible inclusion is welcome.

Community content is available under CC-BY-SA
unless otherwise noted.