HOL (помощник корректора)
Интерактивные системы доказательства теорем
ХОЛ
РазработаноМайкл Дж.С. Гордон
ЛицензияИзмененная (3-пунктная) лицензия BSD
Расширения имени файла.sml
Веб-сайтhol-theorem-prover.org

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

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

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

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

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

Реализации HOL

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

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

Формальные разработки доказательств

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

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

Ссылки

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

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

  • Официальный сайт
  • Документы, определяющие базовую логику HOL
  • HOL4 Описание руководства, включает спецификацию системной логики
  • Виртуальная библиотека формальных методов информации
Получено с "https://en.wikipedia.org/w/index.php?title=HOL_(proof_assistant)&oldid=1237292512"