HOL Light
Proof assistant program
title: "HOL Light" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["free-theorem-provers", "proof-assistants", "free-software-programmed-in-ocaml", "software-using-the-bsd-license"] description: "Proof assistant program" topic_path: "general/free-theorem-provers" source: "https://en.wikipedia.org/wiki/HOL_Light" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0
::summary Proof assistant program ::
HOL Light is a proof assistant for classical higher-order logic. It is a member of the HOL theorem prover family. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is authored and maintained by the mathematician and computer scientist John Harrison. HOL Light is released under the simplified BSD license.
Logical foundations
HOL Light is based on a formulation of type theory with equality as the only primitive notion. The primitive rules of inference are the following: ::data[format=table]
| \cfrac{\Gamma[\alpha_1,\ldots,\alpha_n] \vdash p[\alpha_1,\ldots,\alpha_n]} | INST_TYPE | instantiate type variables in assumptions and conclusion of theorem |
|---|---|---|
| :: |
This formulation of type theory is very close to the one described in section II.2 of .
References
- {{Citation | last1 = Lambek | first1 = J | authorlink1 = Joachim Lambek | last2 = Scott | first2 = P. J. | title = Introduction to Higher Order Categorical logic | publisher = Cambridge University Press | year = 1986 | isbn = 9780521356534 | url-access = registration | url = https://archive.org/details/introductiontohi0000lamb
References
- (13 October 2021). "Jrh13/Hol-light".
::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::