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:
  • 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 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, 24 March 2009.
Further information for possible inclusion is welcome.