Login
Login

HOL Light

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.{{Cite web|url=https://github.com/jrh13/hol-light/|title = Jrh13/Hol-light| website=GitHub |date = 13 October 2021}}

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:

class="wikitable"
style="text-align: center;" | \cfrac{\qquad }{ \vdash t = t}

| style="text-align: center;" | REFL

| reflexivity of equality

style="text-align: center;" | \cfrac{\Gamma \vdash s = t \qquad \Delta \vdash t = u}

{\Gamma \cup \Delta \vdash s = u}

| style="text-align: center;" | TRANS

| transitivity of equality

style="text-align: center;" | \cfrac{\Gamma \vdash f = g \qquad \Delta \vdash x = y}

{\Gamma \cup \Delta \vdash f(x) = g(y)}

| style="text-align: center;" | MK_COMB

| congruence of equality

style="text-align: center;" | \cfrac{\Gamma \vdash s = t}{\Gamma \vdash (\lambda x. s) = (\lambda x. t)}

| style="text-align: center;" | ABS

| abstraction of equality (x must not be free in \Gamma)

style="text-align: center;" | \cfrac{\qquad}{\vdash (\lambda x. t) x = t}

| style="text-align: center;" | BETA

| connection of abstraction and function application

style="text-align: center;" | \cfrac{\qquad }{ \{p\} \vdash p}

| style="text-align: center;" | ASSUME

| assuming p, prove p

style="text-align: center;" | \cfrac{\Gamma \vdash p = q \qquad \Delta \vdash p}

{\Gamma \cup \Delta \vdash q}

| style="text-align: center;" | EQ_MP

| relation of equality and deduction

style="text-align: center;" | \cfrac{\Gamma \vdash p \qquad \Delta \vdash q}

{(\Gamma - \{q\}) \cup (\Delta - \{p\}) \vdash p = q}

| style="text-align: center;" | DEDUCT_ANTISYM_RULE

| deduce equality from 2-way deducibility

style="text-align: center;" | \cfrac{\Gamma[x_1,\ldots,x_n] \vdash p[x_1,\ldots,x_n]}

{\Gamma[t_1,\ldots,t_n] \vdash p[t_1,\ldots,t_n]}

| style="text-align: center;" | INST

| instantiate variables in assumptions and conclusion of theorem

style="text-align: center;" | \cfrac{\Gamma[\alpha_1,\ldots,\alpha_n] \vdash p[\alpha_1,\ldots,\alpha_n]}

{\Gamma[\tau_1,\ldots,\tau_n] \vdash p[\tau_1,\ldots,\tau_n]}

| style="text-align: center;" | 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 {{Harvtxt|Lambek|Scott|1986}}.

References

{{reflist}}

  • {{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

}}

Further reading

  • {{Citation

| author = Freek Wiedijk

| title = Formal Proof — Getting Started

| journal = Notices of the American Mathematical Society

|date=December 2008

| volume = 55

| issue = 11

| pages = 1408–1414

| url = https://www.ams.org/notices/200811/tx081101408p.pdf

| accessdate = 2008-12-14

}}

External links

  • {{Official website|www.cl.cam.ac.uk/~jrh13/hol-light}}

{{ML programming}}

Category:Free theorem provers

Category:Proof assistants

Category:OCaml software