| Isabelle | |
|---|---|
 | |
| Тип | Средство доказательства теорем |
| Разработчик | Lawrence Paulson |
| Написана на | Poly/ML; Scala |
| Операционные системы | GNU/Linux[1], Windows[1] и macOS[1] |
| Первый выпуск | 1 мая 1989 года |
| Аппаратная платформа | кросcплатформенное |
| Последняя версия | Isabelle2021-1 (декабрь 2021) |
| Состояние | активное |
| Лицензия | BSD |
| Сайт | isabelle.in.tum.de |
Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML[2]. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств (хотя это и не обязательно). Как универсальный инструмент, реализует металогику (слабую теорию типов), которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработки в области теории множеств проводились с использованием Isabelle/ZF.
Основным методом реализации доказательства Isabelle является вариант резолюции высшего порядка, основанный на алгоритме унификации высшего порядка. Будучи интерактивной системой, Isabelle также включает в свой состав эффективные инструменты автоматического рассуждения, такие как механизм переписывания термов, решатель методом аналитических таблиц, внешние решатели выполнимости задач в различных теориях, подключаемые через специализированный интерфейс подключения внешних плагинов Sledgehammer, а также внешние инструменты автоматического доказывания теорем, такие как E и SPASS. Isabelle была использована для формализации многочисленных теорем из математики и информатики, таких как теорема Гёделя о полноте, доказательство Гёделя о независимости аксиомы выбора, теоремы о распределении простых чисел. Также Isabelle использовалась для доказательства формальной корректности криптографических протоколов и свойств семантики языков программирования.
Многие из формальных доказательств, полученных с применением Isabelle, доступны публично и хранятся в «Архиве формальных доказательств» (Archive of Formal Proofs), который содержит (по состоянию на 2019 год) не менее 500 статей, включающих в себя более 2 млн строк кода[3].
Распространяется свободно под лицензией BSD. Автор — Лоуренс Полсон (англ. Lawrence Paulson), название дано в честь дочери Жерара Юэ[4].
Пример доказательства
Система позволяет писать доказательства в двух стилях — процедурном и декларативном. Процедурный стиль доказательства задаёт последовательность применения тактик и процедур доказательств. Это соответствует тому стилю, в котором обычно работают обычные математики, но такие доказательства, обычно, достаточно сложны для восприятия, так как при их чтении не очевиден результат, который планируется получить в результате работы такого доказательства.
Декларативные доказательства, реализуемые на специальном встроенном языке доказательств — Isar, — задают конкретные математические процедуры, которые необходимо применить. Они легче читаются и проверяются людьми.
В последних версиях Isabelle процедурный стиль доказательств признан устаревшим. Архив формальных доказательств также рекомендует представлять доказательства в декларативном стиле[5].
Пример декларативного доказательства от противного, написанного на Isar (доказательство подтверждает иррациональность корня квадратного из двух):
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof let ?x = "sqrt (real 2)" assume "?x ∈ ℚ" then obtain m n :: nat where sqrt_rat: "¦?x¦ = real m / real n" and lowest_terms: "coprime m n" by (rule Rats_abs_nat_div_natE) hence "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square) hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce hence "2 dvd m^2" by simp hence "2 dvd m" by simp have "2 dvd n" proof - from ‹2 dvd m› obtain k where "m = 2 * k" .. with eq have "2 * n^2 = 2^2 * k^2" by simp hence "2 dvd n^2" by simp thus "2 dvd n" by simp qed with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False using odd_one by blast qed
Приложения
Isabelle многократно использовалась для реализации формальных методов при спецификации, разработке и верификации программных и аппаратных систем.
В 2009 году, разработчиками проекта L4.verified, реализовывавшегося в австралийском исследовательском центре NICTA впервые было предоставлено формальное доказательство функциональной корректности ядра операционной системы общего назначения, а именно микроядра seL4 (защищенный встроенный вариант L4, способный работать в жёстком реальном времени)[6]. Доказательство было построено и проверено в Isabelle/HOL; оно содержит более 200 тыс. строк сценария верификации для проверки 7500 строк кода Си. Проверка охватывает код, проектирование и реализацию[уточнить]. В рамках доказательства было показано, что код Си правильно реализует формальную спецификацию ядра. Доказательство выявило 144 ошибки в ранней версии кода Си ядра seL4 и примерно по 150 проблем в архитектуре и спецификации самого ядра.
Для языка программирования Lightweight Java с применением Isabelle было получено доказательство типобезопасности[7].
Список исследовательских проектов[8], которые используют Isabelle, ведёт автор системы Полсон.
Альтернативы
Существует ряд схожих с Isabelle по возможностям систем автоматического доказательства теорем, включая:
- Coq, наиболее близкая к Isabelle по возможностям система, но написанная на OCaml
- HOL4, решатель задач, схожий с реализацией логики высшего порядка в Isabelle,
- Mizar system
- Metamath
- Prover9
Примечания
- ↑ 1 2 3 https://isabelle.in.tum.de/
- ↑ Часть новых компонент Isabelle была реализована на Scala
- ↑ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René Archive of Formal Proofs. Дата обращения: 22 октября 2019. Архивировано 19 декабря 2020 года.
- ↑ Gordon, Mike 1.2 History. Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group) (16 ноября 1994). Дата обращения: 28 апреля 2016. Архивировано 5 марта 2017 года.
- ↑ Archive of Formal Proofs. Дата обращения: 12 апреля 2020. Архивировано 19 декабря 2020 года.
- ↑ Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, Montana, US. pp. 207—200. Архивировано из оригинала (PDF) 28 июля 2011. Дата обращения: 12 апреля 2020.
- ↑ afp.sourceforge.net. Дата обращения: 12 апреля 2020. Архивировано 19 марта 2016 года.
- ↑ Projects - Isabelle Community Wiki. Дата обращения: 12 апреля 2020. Архивировано 12 апреля 2020 года.
Литература
- Lawrence C. Paulson The foundation of a generic theorem prover // Journal of Automated Reasoning. — Т. 5, № 3 (September 1989). — С. 363—397. — ISSN 0168-7433.
- Lawrence C. Paulson: The Isabelle Reference Manual.
- M. A. Ozols, K. A. Eastaughffe, and A. Cant. «DOVE: Design Oriented Verification and Evaluation». Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL — A Proof Assistant for Higher-Order Logic.
Ссылки
- Официальный сайт Isabelle
- Isabelle на Stackoverflow
- Архив формальных доказательств
- IsarMathLib — архив формализаций математики, написанных с использованием Isar и базирующихся на ZF-аксиоматике
Эта страница в последний раз была отредактирована 19 декабря 2023 в 13:23.
Обычно почти сразу, изредка в течении часа.