HOL Light

Last updated

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]

Contents

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:

REFLreflexivity of equality
TRANStransitivity of equality
MK_COMBcongruence of equality
ABSabstraction of equality ( must not be free in )
BETAconnection of abstraction and function application
ASSUMEassuming , prove
EQ_MPrelation of equality and deduction
DEDUCT_ANTISYM_RULEdeduce equality from 2-way deducibility
INSTinstantiate variables in assumptions and conclusion of theorem
INST_TYPEinstantiate 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

  1. "Jrh13/Hol-light". GitHub . 13 October 2021.

Further reading