Хол-Лайт

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

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

${\displaystyle {\cfrac {\qquad }{\vdash t=t}}}$	РЕФЛ	рефлексивность равенства
${\displaystyle {\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}}$	ТРАНС	транзитивность равенства
${\displaystyle {\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}}$	МК_КОМБ	соответствие равенства
${\displaystyle {\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda xs)=(\lambda xt)}}}$	АБС	абстракция равенства ( не должна быть свободной )${\displaystyle x}$${\displaystyle \Гамма}$
${\displaystyle {\cfrac {\qquad }{\vdash (\lambda xt)x=t}}}$	БЕТА	связь абстракции и применения функции
${\displaystyle {\cfrac {\qquad }{\{p\}\vdash p}}}$	ПРЕДПОЛАГАТЬ	предполагая , доказывать${\displaystyle p}$${\displaystyle p}$
${\displaystyle {\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}}$	ЭКВ_МП	отношение равенства и вычитания
${\displaystyle {\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}}$	DEDUCT_ANTISYM_RULE	вывести равенство из 2-сторонней выводимости
${\displaystyle {\cfrac {\Гамма [x_{1},\ldots ,x_{n}]\vdash p[x_{1},\ldots ,x_{n}]}{\Гамма [t_{1},\ldots ,t_{n}]\vdash p[t_{1},\ldots ,t_{n}]}}}$	ИНСТ	конкретизировать переменные в предположениях и выводе теоремы
${\displaystyle {\cfrac {\Гамма [\альфа _{1},\ldots,\альфа _{n}]\vdash p[\альфа _{1},\ldots,\альфа _{n}]}{\Гамма [\тау _{1},\ldots,\тау _{n}]\vdash p[\тау _{1},\ldots,\тау _{n}]}}}$	ТИП_ИНСТ	инстанцировать переменные типа в предположениях и выводе теоремы

Эта формулировка теории типов очень близка к той, которая описана в разделе II.2 Ламбека и Скотта (1986).

• Ламбек, Дж.; Скотт, П.Дж. (1986), Введение в категориальную логику высшего порядка , Cambridge University Press, ISBN 9780521356534

• Freek Wiedijk (декабрь 2008 г.), «Формальное доказательство — начало работы» (PDF) , Notices of the American Mathematical Society , 55 (11): 1408–1414 , дата обращения 14 декабря 2008 г.

• Официальный сайт