Isabelle

Isabelle
Тип	Средство доказательства теорем
Разработчик	Lawrence Paulson[англ.]
Написана на	Poly/ML; Scala
Операционные системы	GNU/Linux[2], Windows[2] и macOS[2]
Первый выпуск	1 мая 1989 года
Аппаратная платформа	кросcплатформенное
Последняя версия	Isabelle2021-1 (декабрь 2021; 3 года назад (2021-12))
Читаемые форматы файлов: Isabelle file format[вд][1]
Создаваемые форматы файлов: Isabelle file format[вд][1]
Состояние	активное
Лицензия	BSD
Сайт	isabelle.in.tum.de

Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML^[3]. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств (хотя это и не обязательно). Как универсальный инструмент, реализует металогику (слабую теорию типов), которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработки в области теории множеств проводились с использованием Isabelle/ZF.

Основным методом реализации доказательства Isabelle является вариант резолюции высшего порядка, основанный на алгоритме унификации высшего порядка. Будучи интерактивной системой, Isabelle также включает в свой состав эффективные инструменты автоматического рассуждения, такие как механизм переписывания термов, решатель методом аналитических таблиц, внешние решатели выполнимости задач в различных теориях, подключаемые через специализированный интерфейс подключения внешних плагинов Sledgehammer, а также внешние инструменты автоматического доказывания теорем, такие как E^[англ.] и SPASS^[англ.]. Isabelle была использована для формализации многочисленных теорем из математики и информатики, таких как теорема Гёделя о полноте, доказательство Гёделя о независимости аксиомы выбора, теоремы о распределении простых чисел. Также Isabelle использовалась для доказательства формальной корректности криптографических протоколов и свойств семантики языков программирования.

Многие из формальных доказательств, полученных с применением Isabelle, доступны публично и хранятся в «Архиве формальных доказательств» (Archive of Formal Proofs), который содержит (по состоянию на 2019 год) не менее 500 статей, включающих в себя более 2 млн строк кода^[4].

Распространяется свободно под лицензией BSD. Автор — Лоуренс Полсон (англ. Lawrence Paulson), название дано в честь дочери Жерара Юэ^[5].

1. ↑ ^{1 2} https://isabelle.in.tum.de/dist/Isabelle2024/doc/prog-prove.pdf
2. ↑ ^{1 2 3} https://isabelle.in.tum.de/
3. ↑ Часть новых компонент Isabelle была реализована на Scala
4. ↑ Nipkow, Tobias; Eberl, Manuel; Klein, Gerwin; Paulson, Larry; Thiemann, René. Archive of Formal Proofs  (неопр.). Дата обращения: 22 октября 2019. Архивировано 19 декабря 2020 года.
5. ↑ Gordon, Mike. 1.2 History  (неопр.). Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group) (16 ноября 1994). Дата обращения: 28 апреля 2016. Архивировано 5 марта 2017 года.