HOL Light 

HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations.

Logical foundations

HOL Light is based on a formulation of type theory with equality as the only primitive concept. The primitive rules of inference are the following:

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

References

Lambek, J; P. J. Scott (1986). Introduction to Higher Order Categorical logic. Cambridge University Press. 

External links