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