HOL Light

From Wikipedia, the free encyclopedia

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.

[edit] 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