HOL Light is a
proof assistant for classical
higher-order logic
In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...
. 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
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
with equality
as the only
primitive notion. The primitive rules of inference
are the following:
This formulation of type theory is very close to the one described in
section II.2 of .
References
*
Further reading
*
External links
*
{{ML programming
Free theorem provers
Proof assistants
OCaml software