HOL Light - HOL Light

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

Логические основы

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	создавать экземпляры переменных типа в предположениях и заключении теоремы