HOL (ассистент по корректуре)
-
Основы HOL
- HOL — семейство интерактивных систем доказательства теорем на основе логики высшего порядка.
- Системы HOL следуют подходу LCF и реализованы как библиотеки с абстрактными типами данных.
- Доказанные теоремы должны быть верными при условии корректной реализации функций в библиотеке.
-
Логика и реализации
- Системы HOL используют классическую логику высшего порядка с простыми аксиомами.
- HOL provers тесно связаны с Isabelle/HOL, наиболее широко используемой логикой Isabelle.
- HOL4 — текущая поддерживаемая система, основанная на HOL88, с реализацией на ML.
- После HOL88 системы HOL90, hol98 и HOL4 реализованы на стандартном ML, с возможностью выбора между Moscow ML и Poly/ML.
-
Дополнительные системы и лицензии
- HOL Light — экспериментальная версия с простой логикой, теперь на OCaml, с лицензией BSD.
- ProofPower — набор инструментов для работы с Z-нотациями, с 5 инструментами под лицензией GPL v2 и одним под проприетарной лицензией.
- HOL Zero — минималистичная реализация с акцентом на надежность, с лицензией GPL 3+.
- Candle — проверенная реализация HOL Light на CakeML.
-
Применение в формальных доказательствах
- HOL использовался для разработки компилятора для ML и реализации Lisp на различных архитектурах.
- HOL также применялся для формализации семантики многопроцессорных архитектур и машинного кода.
-
Рекомендации
- Ссылки на официальный веб-сайт, документы по базовой логике HOL, руководство по HOL4 и информацию о формальных методах виртуальной библиотеки.
Полный текст статьи: