Из Википедии, бесплатной энциклопедии
  (Перенаправлено с HOL4 )
Перейти к навигации Перейти к поиску
HOL
РазработаноМайкл Дж. К. Гордон
ЛицензияМодифицированная (3 пункта) лицензия BSD
Расширения имени файла.sml
Веб-сайтпрограмма доказательства теорем .org

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]

Ссылки [ править ]

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

Дальнейшее чтение [ править ]

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

Внешние ссылки [ править ]

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