Разработано | Майкл Дж. К. Гордон |
---|---|
Лицензия | Модифицированная (3 пункта) лицензия BSD |
Расширения имени файла | .sml |
Веб-сайт | программа доказательства теорем |
HOL ( логика высшего порядка ) обозначает семейство интерактивных систем доказательства теорем, использующих сходные (более высокого порядка) логику и стратегии реализации. Системы в этом семействе следуют подходу LCF, поскольку они реализованы в виде библиотеки на каком-то языке программирования. Эта библиотека реализует абстрактный тип данных доказанных теорем, поэтому новые объекты этого типа могут быть созданы только с использованием функций в библиотеке, которые соответствуют правилам вывода в логике более высокого порядка.. Пока эти функции реализованы правильно, все теоремы, доказанные в системе, должны быть верными. Таким образом, большая система может быть построена на небольшом доверенном ядре.
В системах семейства HOL используется язык программирования ML или его последователи. Изначально ML был разработан вместе с LCF, чтобы служить метаязыком для систем доказательства теорем; Фактически, это название означает «Мета-язык».
Основная логика [ править ]
Системы HOL используют варианты классической логики высшего порядка , которая имеет простые аксиоматические основы с небольшим количеством аксиом и хорошо понятной семантикой. [1]
Логика, используемая в пруверах HOL, тесно связана с логикой Isabelle / HOL [2], наиболее широко используемой логикой Изабель .
Члены семейства испытателей HOL [ править ]
Есть четыре системы HOL (использующие, по сути, одну и ту же логику), которые все еще поддерживаются и развиваются.
- Первый, HOL4, происходит от системы HOL88, которая стала кульминацией первоначальных усилий по реализации HOL под руководством Майка Гордона . HOL88 включал собственную реализацию ML, которая, в свою очередь, была реализована поверх Common Lisp . Все реализации, следующие за HOL88 (HOL90, hol98 и HOL4), использовали в качестве языка реализации Standard ML . Система hol98 привязана к московской реализации стандартного машинного обучения ; HOL4 может быть построен с использованием Moscow ML или Poly / ML.. Из этих четырех систем поддерживается и развивается только HOL4. Все они поставляются с большими библиотеками кода доказательства теорем. Они реализуют дополнительную автоматизацию поверх очень простого основного кода. 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]
Хотя HOL является предшественником Isabelle , различные производные HOL, такие как HOL4 и HOL Light, остаются активными и используются.
Избранные формальные разработки доказательств [ править ]
Проект CakeML [7] разработал официально зарекомендовавший себя компилятор для ML . Ранее HOL использовался для разработки официально проверенной реализации LISP, работающей на ARM, x86 и PowerPC. [8]
HOL также использовался для разработки формальной семантики для мультипроцессоров x86 [9], а также семантики машинного кода для архитектур Power ISA и ARM . [10]
Ссылки [ править ]
- ^ Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство . Прикладная логика. 27 (Второе изд.). Дордрехт: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
- ^ Тобиас Нипков ; Маркус Венцель; Лоуренс К. Полсон (2002). Изабель / ХОЛ: помощник по проверке логики высокого порядка . Берлин, Гейдельберг: Springer-Verlag. ISBN 978-3-540-45949-1.
- ^ "Интерактивное средство доказательства теорем HOL" .
- ^ "HOL Light" .
- ^ "Получение ProofPower" .
- ^ См. Файл ЛИЦЕНЗИИ в архиве. Архивировано 3 марта 2012 г. на Wayback Machine .
- ^ "CakeML" .
- ^ Магнус О. Майрин; Майкл Дж. К. Гордон. Проверенные реализации LISP на ARM, x86 и PowerPC (PDF) . TPHOLs 2009. С. 359–374.
- ^ Питер Сьюэлл; Сусмит Саркар; Скотт Оуэнс; Франческо Заппа Нарделли; Магнус О. Майрин (2010). «x86-TSO: строгая и удобная модель программиста для мультипроцессоров x86» (PDF) . Коммуникации ACM . 53 (7): 89–97. DOI : 10.1145 / 1785414.1785443 .
- ^ Джейд Алглав; Энтони Си Джей Фокс; Самин Иштиак; Магнус О. Майрин; Сусмит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и ARM многопроцессорный машинный код (PDF) . DAMP 2009. С. 13–24.
Дальнейшее чтение [ править ]
- Гордон, Майкл JC (1996). «От LCF к HOL: краткая история» . Проверено 11 октября 2007 .
Внешние ссылки [ править ]
- Домашняя страница проекта HOL4
- Документы, определяющие базовую логику HOL
- Руководство HOL4 Description , которое включает спецификацию логики системы.
- Информация о формальных методах виртуальной библиотеки