HOL (помощник по проверке)

ГДЕ
Разработано	Майкл Джей Си Гордон
Лицензия	Модифицированная (3 пункта) лицензия BSD
Расширения имен файлов	.sml
Веб-сайт	хол-теорема-доказательство .org

HOL ( логика высшего порядка ) обозначает семейство интерактивных систем доказательства теорем, использующих аналогичную логику (высшего порядка) и стратегии реализации. Системы этого семейства следуют подходу LCF , поскольку они реализованы в виде библиотеки, которая определяет абстрактный тип данных доказанных теорем, так что новые объекты этого типа могут быть созданы только с использованием функций в библиотеке, которые соответствуют правилам вывода более высокого порядка. логика . Пока эти функции правильно реализованы, все доказанные в системе теоремы должны быть справедливы. Таким образом, большая система может быть построена на основе небольшого доверенного ядра.

Системы семейства HOL используют ML или его преемников. Первоначально ML был разработан вместе с LCF как метаязык для систем доказательства теорем; на самом деле это название означает «Мета-язык».

Основная логика

Системы HOL используют варианты классической логики высшего порядка , которая имеет простые аксиоматические основы с небольшим количеством аксиом и хорошо понятной семантикой. ^[1]

Логика, используемая в пруверах HOL, тесно связана с Isabelle/HOL. ^[2] наиболее широко используемая логика Изабель .

Реализации HOL

Ряд систем HOL (по сути, имеющих одну и ту же логику) остаются активными и используются:

HOL4 — единственная в настоящее время поддерживаемая и разрабатываемая система, основанная на системе HOL88, которая стала кульминацией первоначальных усилий по внедрению HOL, возглавляемых Майком Гордоном . HOL88 включал собственную реализацию машинного обучения , которая, в свою очередь, была реализована поверх Common Lisp . Все системы, последовавшие за HOL88 (HOL90, hol98 и HOL4), были реализованы на стандартном ML ; в то время как hol98 связан с Moscow ML , HOL4 может быть построен либо с помощью Moscow ML, либо с Poly/ML . Все они поставляются с большими библиотеками кода доказательства теорем, которые реализуют дополнительную автоматизацию поверх очень простого основного кода. HOL4 имеет лицензию BSD. ^[3]
HOL Light — экспериментальная «минималистская» версия HOL, которая с тех пор превратилась в еще один массовый вариант HOL; ее логические основы остаются необычайно простыми. HOL Light, изначально реализованный в Caml Light , теперь использует OCaml . HOL Light доступен по новой лицензии BSD. ^[4]
ProofPower — набор инструментов, предназначенных для обеспечения специальной поддержки работы с обозначением Z для формальной спецификации. 5 из 6 инструментов имеют лицензию GNU GPL v2. Шестой (PPDaz) имеет собственную лицензию. ^[5]
HOL Zero — минималистская реализация, ориентированная на надежность. HOL Zero имеет лицензию GNU GPL 3+. ^[6]
Candle — сквозная проверенная реализация HOL Light поверх CakeML. ^[7]

Официальные доказательства развития

Проект CakeML разработал формально проверенный компилятор для машинного обучения. ^[8] Ранее HOL использовался для разработки официально проверенной реализации Lisp , работающей на ARM, x86 и PowerPC. ^[9]

HOL также использовался для формализации семантики мультипроцессоров x86. ^[10] а также машинный код для Power ISA и ARM . архитектур ^[11]

Ссылки

^ Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство . Серия «Прикладная логика». Том. 27 (Второе изд.). Дордрехт: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7 .
^ Тобиас Нипков ; Маркус Венцель; Лоуренс К. Полсон (2002). Изабель/HOL: Помощник по доказательству логики высшего порядка . Берлин, Гейдельберг: Springer-Verlag. ISBN 978-3-540-45949-1 .
^ «Интерактивное средство доказательства теорем HOL» .
^ «ХОЛ Лайт» .
^ «Получение ProofPower» .
^ См. файл ЛИЦЕНЗИИ в архиве , заархивированный 3 марта 2012 г. на Wayback Machine .
^ Абрахамссон, Оскар; Мирин, Магнус О.; Кумар, Рамана; Сьюэлл, Томас (2022). Андроник, июнь; де Моура, Леонардо (ред.). «Свеча: проверенная реализация HOL Light» . 13-я Международная конференция по интерактивному доказательству теорем (ITP 2022) . Международные труды Лейбница по информатике (LIPIcs). 237 . Дагштуль, Германия: Замок Дагштуль – Центр информатики Лейбница: 3:1–3:17. дои : 10.4230/LIPIcs.ITP.2022.3 . ISBN 978-3-95977-252-5 . S2CID 251323103 .
^ «ТортМЛ» .
^ Магнус О. Мирин; Майкл Джей Си Гордон. Проверенные реализации LISP на ARM, x86 и PowerPC (PDF) . TPHOLs 2009. стр. 359–374.
^ Питер Сьюэлл; Сумит Саркар; Скотт Оуэнс; Франческо Заппа Нарделли; Магнус О. Мирин (2010). «x86-TSO: строгая и удобная модель программиста для мультипроцессоров x86» (PDF) . Коммуникации АКМ . 53 (7): 89–97. дои : 10.1145/1785414.1785443 . S2CID 1999974 .
^ Джейд Алглав ; Энтони Си Джей Фокс; Самин Иштиак; Магнус О. Мирин; Сумит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и многопроцессорного машинного кода ARM (PDF) . DAMP 2009. стр. 13–24.

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

Гордон, Майкл Дж. К. (1996). «От LCF к HOL: Краткая история» . Проверено 11 октября 2007 г.

Внешние ссылки

Официальный сайт
Документы, определяющие базовую логику HOL.
Руководство по описанию HOL4 , включает спецификацию системной логики.
Информация о формальных методах виртуальной библиотеки

[1] Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство . Серия «Прикладная логика». Том. 27 (Второе изд.). Дордрехт: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7 .

[2] Тобиас Нипков ; Маркус Венцель; Лоуренс К. Полсон (2002). Изабель/HOL: Помощник по доказательству логики высшего порядка . Берлин, Гейдельберг: Springer-Verlag. ISBN 978-3-540-45949-1 .

[3] «Интерактивное средство доказательства теорем HOL» .

[4] «ХОЛ Лайт» .

[5] «Получение ProofPower» .

[6] См. файл ЛИЦЕНЗИИ в архиве , заархивированный 3 марта 2012 г. на Wayback Machine .

[7] Абрахамссон, Оскар; Мирин, Магнус О.; Кумар, Рамана; Сьюэлл, Томас (2022). Андроник, июнь; де Моура, Леонардо (ред.). «Свеча: проверенная реализация HOL Light» . 13-я Международная конференция по интерактивному доказательству теорем (ITP 2022) . Международные труды Лейбница по информатике (LIPIcs). 237 . Дагштуль, Германия: Замок Дагштуль – Центр информатики Лейбница: 3:1–3:17. дои : 10.4230/LIPIcs.ITP.2022.3 . ISBN 978-3-95977-252-5 . S2CID 251323103 .

[8] «ТортМЛ» .

[9] Магнус О. Мирин; Майкл Джей Си Гордон. Проверенные реализации LISP на ARM, x86 и PowerPC (PDF) . TPHOLs 2009. стр. 359–374.

[10] Питер Сьюэлл; Сумит Саркар; Скотт Оуэнс; Франческо Заппа Нарделли; Магнус О. Мирин (2010). «x86-TSO: строгая и удобная модель программиста для мультипроцессоров x86» (PDF) . Коммуникации АКМ . 53 (7): 89–97. дои : 10.1145/1785414.1785443 . S2CID 1999974 .

[11] Джейд Алглав ; Энтони Си Джей Фокс; Самин Иштиак; Магнус О. Мирин; Сумит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и многопроцессорного машинного кода ARM (PDF) . DAMP 2009. стр. 13–24.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]