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:
REFL | reflexivity of equality | |
![]() |
TRANS | transitivity of equality |
![]() |
MK_COMB | congruence of equality |
![]() |
ABS | abstraction of equality ( must not be free in ) |
![]() |
BETA | connection of abstraction and function application |
![]() |
ASSUME | assuming, prove |
![]() |
EQ_MP | relation of equality and deduction |
![]() |
DEDUCT_ANTISYM_RULE | deduce equality from 2-way deducibility |
![]() |
INST | instantiate variables in assumptions and conclusion of theorem |
![]() |
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).
Read more about this topic: HOL Light
Famous quotes containing the words logical and/or foundations:
“I see mysteries and complications wherever I look, and I have never met a steadily logical person.”
—Martha Gellhorn (b. 1908)
“These, in the day when heaven was falling,
The hour when earths foundations fled,
Followed their mercenary calling
And took their wages and are dead.”
—A.E. (Alfred Edward)
Related Phrases
Related Words