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
- ↑ "Jrh13/Hol-light". 13 October 2021. https://github.com/jrh13/hol-light/.
- Lambek, J; Scott, P. J. (1986), Introduction to Higher Order Categorical logic, Cambridge University Press, ISBN 9780521356534, https://archive.org/details/introductiontohi0000lamb
Further reading
- Freek Wiedijk (December 2008), "Formal Proof — Getting Started", Notices of the American Mathematical Society 55 (11): 1408–1414, https://www.ams.org/notices/200811/tx081101408p.pdf, retrieved 2008-12-14
External links
Original source: https://en.wikipedia.org/wiki/HOL Light.
Read more |