HOL Light

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

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

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

${\ Displaystyle {\ cfrac {\ qquad} {\ vdash т = т}}}$	REFL	рефлексивность равенства
${\ 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)}}}$	MK_COMB	соответствие равенства
${\ Displaystyle {\ cfrac {\ Gamma \ vdash s = t} {\ Gamma \ vdash (\ lambda xs) = (\ lambda xt)}}}$	АБС	абстракция равенства ( не должна быть свободной )${\ displaystyle x}$${\ displaystyle \ Gamma}$
${\ 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}}}$	EQ_MP	отношение равенства и дедукции
${\displaystyle {\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}}$	DEDUCT_ANTISYM_RULE	вывести равенство из двусторонней выводимости
${\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}]}}}$	INST	экземпляры переменных в предположениях и заключении теоремы
${\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}]}}}$	INST_TYPE	создавать экземпляры переменных типа в предположениях и заключении теоремы

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

Ссылки [ править ]

• Lambek, J ; Скотт, П.Дж. (1986), Введение в категориальную логику высшего порядка , Cambridge University Press, ISBN 9780521356534 CS1 maint: discouraged parameter (link)

Дальнейшее чтение [ править ]

• Фрик Wiedijk (декабрь 2008), "Формальное доказательство - Начало работы" (PDF) , Уведомление о Американских математическом обществе , 55 (11): 1408-1414 , извлекаться 2008-12-14 CS1 maint: discouraged parameter (link)

Внешние ссылки [ править ]

• HOL Light