HOL Light is a member of the

HOL theorem prover family HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defin ...

. Like the other members, it is a

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

for classical

higher order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...

. 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 John Harrison ( – 24 March 1776) was a self-educated English carpenter and clockmaker who invented the marine chronometer, a long-sought-after device for solving the problem of calculating longitude while at sea. Harrison's solution revol ...

. HOL Light is released under the

simplified BSD license BSD licenses are a family of permissive free software licenses, imposing minimal restrictions on the use and distribution of covered software. This is in contrast to copyleft licenses, which have share-alike requirements. The original BSD li ...

Logical foundations

HOL Light is based on a formulation of

type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...

with equality as the only

primitive notion In mathematics, logic, philosophy, and formal systems, a primitive notion is a concept that is not defined in terms of previously-defined concepts. It is often motivated informally, usually by an appeal to intuition and everyday experience. In an ...

. 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

External links

HOL Light
Free theorem provers Proof assistants OCaml software

Logical foundations

References

Further reading

External links