Jump to content

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

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

HOL ( логика высшего порядка ) обозначает семейство интерактивных систем доказательства теорем, использующих аналогичную логику (высшего порядка) и стратегии реализации. Системы этого семейства следуют подходу LCF , поскольку они реализованы в виде библиотеки, которая определяет абстрактный тип данных доказанных теорем, так что новые объекты этого типа могут быть созданы только с использованием функций в библиотеке, которые соответствуют правилам вывода более высокого порядка. логика . Пока эти функции правильно реализованы, все доказанные в системе теоремы должны быть справедливы. Таким образом, большая система может быть построена на основе небольшого доверенного ядра.

Системы семейства HOL используют ML или его преемников. Первоначально ML был разработан вместе с LCF как метаязык для систем доказательства теорем; на самом деле это название означает «Мета-язык».

Основная логика

[ редактировать ]

Системы HOL используют варианты классической логики высшего порядка , которая имеет простые аксиоматические основы с небольшим количеством аксиом и хорошо понятной семантикой. [1]

Логика, используемая в пруверах HOL, тесно связана с Isabelle/HOL. [2] наиболее широко используемая логика Изабель .

Реализации HOL

[ редактировать ]

Ряд систем HOL (по сути, имеющих одну и ту же логику) остаются активными и используются:

  1. HOL4 — единственная в настоящее время поддерживаемая и разрабатываемая система, основанная на системе HOL88, которая стала кульминацией первоначальных усилий по внедрению HOL, возглавляемых Майком Гордоном . HOL88 включал собственную реализацию машинного обучения , которая, в свою очередь, была реализована поверх Common Lisp . Все системы, последовавшие за HOL88 (HOL90, hol98 и HOL4), были реализованы на стандартном ML ; в то время как hol98 связан с Moscow ML , HOL4 может быть построен либо с помощью Moscow ML, либо с Poly/ML . Все они поставляются с большими библиотеками кода доказательства теорем, которые реализуют дополнительную автоматизацию поверх очень простого основного кода. HOL4 имеет лицензию BSD. [3]
  2. HOL Light — экспериментальная «минималистская» версия HOL, которая с тех пор превратилась в еще один массовый вариант HOL; ее логические основы остаются необычайно простыми. HOL Light, изначально реализованный в Caml Light , теперь использует OCaml . HOL Light доступен по новой лицензии BSD. [4]
  3. ProofPower — набор инструментов, предназначенных для обеспечения специальной поддержки работы с обозначением Z для формальной спецификации. 5 из 6 инструментов имеют лицензию GNU GPL v2. Шестой (PPDaz) имеет собственную лицензию. [5]
  4. HOL Zero — минималистская реализация, ориентированная на надежность. HOL Zero имеет лицензию GNU GPL 3+. [6]
  5. Candle — сквозная проверенная реализация HOL Light поверх CakeML. [7]

Официальные доказательства развития

[ редактировать ]

Проект CakeML разработал формально проверенный компилятор для машинного обучения. [8] Ранее HOL использовался для разработки официально проверенной реализации Lisp , работающей на ARM, x86 и PowerPC. [9]

HOL также использовался для формализации семантики мультипроцессоров x86. [10] а также машинный код для Power ISA и ARM . архитектур [11]

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

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

[ редактировать ]
[ редактировать ]
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 90d48b8b078dbefe64cc9daacad04134__1722208920
URL1:https://arc.ask3.ru/arc/aa/90/34/90d48b8b078dbefe64cc9daacad04134.html
Заголовок, (Title) документа по адресу, URL1:
HOL (proof assistant) - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)