ХОЛ Лайт

HOL Light — помощник для доказательства классической логики высшего порядка . Он является членом семейства средств доказательства теорем HOL . По сравнению с другими системами HOL, HOL Light имеет относительно простую основу. HOL Light создан и поддерживается математиком и ученым-компьютерщиком Джоном Харрисоном. HOL Light выпускается под упрощенной лицензией BSD . ^[1]

Логические основы [ править ]

HOL Light основан на формулировке теории типов с равенством как единственное примитивное понятие . Примитивные правила вывода следующие:

${\cfrac {\qquad }{\vdash t=t}}$	РЕФЛ	рефлексивность равенства
${\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}$	ТРАНС	транзитивность равенства
${\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}$	МК_КОМБ	соответствие равенства
${\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda x.s)=(\lambda x.t)}}$	АБС	абстракция равенства ( $x$ не должен быть свободным в $\Gamma$ )
${\cfrac {\qquad }{\vdash (\lambda x.t)x=t}}$	БЕТА	соединение абстракции и применения функции
${\cfrac {\qquad }{\{p\}\vdash p}}$	ПРЕДПОЛАГАТЬ	предполагая $p$ , доказывать $p$
${\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}$	EQ_MP	отношение равенства и дедукции
${\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}$	DEDUCT_ANTISYM_RULE	вывести равенство из двусторонней выводимости
${\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}]}}$	ИНСТ	создавать экземпляры переменных в предположениях и заключении теоремы
${\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	создавать экземпляры переменных типа в предположениях и заключении теоремы