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

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), использовали Стандартный ML как язык реализации. Система hol98 привязана к Москва МЛ реализация Стандартный ML; HOL4 может быть построен с Москва МЛ или Поли / 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 является предшественником Изабель различные производные HOL, такие как HOL4 и HOL Light, остаются активными и используются.

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

CakeML[7] проект разработал официально проверенный компилятор для ML. Раньше HOL использовался для разработки официально проверенного LISP реализация работает на ARM, x86 и PowerPC.[8]

HOL также использовался для разработки формальной семантики для мультипроцессоров x86,[9] а также семантика машинного кода для Питание ISA и РУКА архитектуры.[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. ^ См. Файл LICENSE в tarball В архиве 2012-03-03 в 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. Дои:10.1145/1785414.1785443.
  10. ^ Джейд Алглав; Энтони С. Дж. Фокс; Самин Иштиак; Магнус О. Майрин; Сусмит Саркар; Питер Сьюэлл; Франческо Заппа Нарделли. Семантика Power и многопроцессорный машинный код ARM (PDF). DAMP 2009. С. 13–24.

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

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