Войти
 Isabelle / jEdit работает на macOS | |
| Оригинальный автор (-ы) | Лоуренс Полсон |
|---|---|
| Разработчик (и) | Кембриджский университет и Мюнхенский технический университет и др. |
| Первоначальный выпуск | 1986 |
| Стабильный выпуск | 2019 / июнь 2019 |
| Написано на | Standard ML и Scala |
| Операционная система | Linux, Windows, Mac OS X |
| Тип | Математика |
| Лицензия | Лицензия BSD |
| Веб-сайт | isabelle.in.tum.de |
The Isabelle автоматическое средство доказательства теорем - это интерактивное средство доказательства теорем, средство доказательства теорем с логикой высшего порядка (HOL). Это средство доказательства теорем в стиле LCF (написано в Standard ML ). Таким образом, он основан на небольшом логическом ядре (ядре) для повышения надежности доказательств, не требуя (но поддерживая) явные объекты доказательства.
Isabelle является универсальным: она обеспечивает мета-логику (слабая теория типов ), которая используется для кодирования логики объекта, такой как первого порядка. логика (FOL), логика высшего порядка (HOL) или теория множеств Цермело – Френкеля (ZFC). Наиболее широко используемой объектной логикой является Isabelle / HOL, хотя значительные разработки теории множеств были завершены в Isabelle / ZF. Основной метод проверки Изабель - это версия разрешения более высокого порядка, основанная на унификации.
. Несмотря на интерактивность, Изабель имеет эффективные инструменты автоматического мышления, такие как переписывание терминов и механизм доказательства таблиц, различные процедуры принятия решений и, через интерфейс Sledgehammer и автоматизацию доказательства, внешние решатели теорий выполнимости по модулю (SMT) (включая CVC4 ) и разрешение на основе автоматических средств доказательства теорем (ATP), включая E и SPASS (Метод доказательства Metis восстанавливает доказательства разрешающей способности, сгенерированные этими ATP). Он также имеет два модуля поиска модели (генераторы контрпримера ): Nitpick и Nunchaku .
Изабель имеет локали, которые являются модулями. которые структурируют большие доказательства. Локаль фиксирует типы, константы и допущения в пределах указанной области, поэтому их не нужно повторять для каждой леммы.
Isar («понятное полуавтоматическое обоснование ») - это формальный язык доказательств Изабель. Он вдохновлен системой Мицара.
Изабель использовалась для формализации множества теорем из математики и информатики, таких как теорема Гёделя о полноте, Теорема Гёделя о непротиворечивости аксиомы выбора , теоремы о простых числах, корректности протоколов безопасности и свойств семантики языка программирования. Многие формальные доказательства хранятся в Архиве формальных доказательств, который содержит (по состоянию на 2019 год) не менее 500 статей с более чем 2 миллионами строк доказательства.
Программа доказательства теорем Изабель бесплатна программное обеспечение, выпущенное под пересмотренной лицензией BSD.
Изабель была названа Лоуренсом Полсоном в честь дочери Жерара Юэ.
Изабель позволяет писать доказательства в двух разных стилях: процедурный и декларативный. Процедурные доказательства определяют серию (доказательство теорем функций / процедур ), которые необходимо применить; отражая процедуру, которую математик-человек мог бы применить для доказательства результата, они, как правило, трудны для чтения, поскольку не описывают результат этих шагов. Декларативные доказательства (поддерживаемые языком доказательств Изабель, Isar), с другой стороны, определяют фактические математические операции, которые должны быть выполнены, и поэтому люди легче читают и проверяют их.
В последних версиях Isabelle процедурный стиль устарел.
Например, декларативное доказательство противоречия в Isar, что квадратный корень из двух не является рациональным, можно записать следующим образом.
теорема sqrt2_not_rational: "sqrt 2 ∉ ℚ" доказательство let? X = "sqrt 2" принять "? X ∈ ℚ", затем получить mn :: nat, где sqrt_rat: "¦? X¦ = m / n" и low_terms: "coprime mn" по (правило Rats_abs_nat_div_natE), следовательно, "m ^ 2 =? x ^ 2 * n ^ 2" по (auto simp add: power2_eq_square), следовательно, eq: "m ^ 2 = 2 * n ^ 2" с использованием of_nat_eq_iff power2_eq_square на fastforce, следовательно, "2 dvd m ^ 2" от simp, следовательно, "2 dvd m" от simp имеет доказательство "2 dvd n" - из ‹2 dvd m› получить k, где "m = 2 * k".. с eq иметь "2 * n ^ 2 = 2 ^ 2 * k ^ 2 "по simp, следовательно," 2 dvd n ^ 2 "по simp, таким образом," 2 dvd n "по simp qed с‹ 2 dvd m ›имеют" 2 dvd gcd mn "по (правилу gcd_greatest) с наименьшими_термами имеет "2 dvd 1" по simp, таким образом, False с использованием odd_one по blast qed
Изабель использовалась для помощи формальным методам для спецификации, разработки и проверка программно-аппаратных комплексов.
Ларри Полсон ведет список исследовательских проектов, в которых используется Isabelle.
Несколько Помощники по проверке предоставляют аналогичные функциональные возможности Изабель, включая:
Портал бесплатного программного обеспечения с открытым исходным кодом 