Software:HOL Light

From HandWiki

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.[1]

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:

[math]\displaystyle{ \cfrac{\qquad }{ \vdash t = t} }[/math] REFL reflexivity of equality
[math]\displaystyle{ \cfrac{\Gamma \vdash s = t \qquad \Delta \vdash t = u} {\Gamma \cup \Delta \vdash s = u} }[/math] TRANS transitivity of equality
[math]\displaystyle{ \cfrac{\Gamma \vdash f = g \qquad \Delta \vdash x = y} {\Gamma \cup \Delta \vdash f(x) = g(y)} }[/math] MK_COMB congruence of equality
[math]\displaystyle{ \cfrac{\Gamma \vdash s = t}{\Gamma \vdash (\lambda x. s) = (\lambda x. t)} }[/math] ABS abstraction of equality ([math]\displaystyle{ x }[/math] must not be free in [math]\displaystyle{ \Gamma }[/math])
[math]\displaystyle{ \cfrac{\qquad}{\vdash (\lambda x. t) x = t} }[/math] BETA connection of abstraction and function application
[math]\displaystyle{ \cfrac{\qquad }{ \{p\} \vdash p} }[/math] ASSUME assuming [math]\displaystyle{ p }[/math], prove [math]\displaystyle{ p }[/math]
[math]\displaystyle{ \cfrac{\Gamma \vdash p = q \qquad \Delta \vdash p} {\Gamma \cup \Delta \vdash q} }[/math] EQ_MP relation of equality and deduction
[math]\displaystyle{ \cfrac{\Gamma \vdash p \qquad \Delta \vdash q} {(\Gamma - \{q\}) \cup (\Delta - \{p\}) \vdash p = q} }[/math] DEDUCT_ANTISYM_RULE deduce equality from 2-way deducibility
[math]\displaystyle{ \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]} }[/math] INST instantiate variables in assumptions and conclusion of theorem
[math]\displaystyle{ \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]} }[/math] 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 (Lambek Scott).

References

Further reading

External links