WikiDer > HOL Light

HOL Light

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

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

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

REFLрефлексивность равенства
ТРАНСтранзитивность равенства
MK_COMBсоответствие равенства
АБСабстракция равенства ( не должен быть свободным в )
БЕТАсоединение абстракции и приложения функции
ПРЕДПОЛАГАТЬпредполагая , доказывать
EQ_MPотношение равенства и дедукции
DEDUCT_ANTISYM_RULEвывести равенство из двухсторонней выводимости
INSTэкземпляры переменных в предположениях и заключении теоремы
INST_TYPEэкземпляры переменных типа в предположениях и заключении теоремы

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

Рекомендации

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

дальнейшее чтение

внешняя ссылка