Изабель (ассистент корректора)
Автоматизированное устройство доказательства теорем на основе логики высшего порядка (HOL)
Изабель
Оригинальный автор(ы)Лоуренс Полсон
Разработчик(и)Кембриджский университет ,
Мюнхенский технический университет и др.
Первоначальный выпуск1986 ; 38 лет назад [1] ( 1986 )
Стабильный релиз
Isabelle2024 / Май 2024 ; 6 месяцев назад ( 2024-05 )
Написано вСтандартный ML , Scala
Операционная системаLinux , Windows , MacOS
ТипМатематика
ЛицензияБСД
Веб-сайтisabelle.in.tum.de

Автоматизированный доказатель теорем Isabelle [a] — это доказатель теорем логики высшего порядка (HOL) , написанный на Standard ML и Scala . Как доказатель теорем в стиле Logic for Computable Functions (LCF), он основан на небольшом логическом ядре (ядре) для повышения достоверности доказательств, не требуя, но поддерживая, явные объекты доказательств.

Isabelle доступен в гибкой системной структуре, позволяющей логически безопасные расширения, которые включают как теории, так и реализации для генерации кода, документирования и специальной поддержки для различных формальных методов . Его можно рассматривать как интегрированную среду разработки (IDE) для формальных методов. В последние годы значительное количество теорий и расширений систем было собрано в Архиве формальных доказательств Isabelle ( Isabelle AFP ) [2]

Изабель была названа Лоуренсом Полсоном в честь дочери Жерара Юэ . [3]

Доказательство теоремы Изабеллы — это свободное программное обеспечение , выпущенное под пересмотренной лицензией BSD .

Функции

Isabelle является обобщенной: она предоставляет металогику (слабую теорию типов ), которая используется для кодирования объектных логик, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело–Френкеля (ZFC). Наиболее широко используемой объектной логикой является Isabelle/HOL, хотя значительные разработки теории множеств были завершены в Isabelle/ZF. Основной метод доказательства Isabelle — это версия резолюции высшего порядка, основанная на объединении высшего порядка .

Несмотря на интерактивность, Isabelle предлагает эффективные инструменты автоматического рассуждения, такие как механизм переписывания терминов и доказатель таблиц , различные процедуры принятия решений и, через интерфейс автоматизации доказательств Sledgehammer , решатели внешних теорий выполнимости по модулю (SMT) (включая CVC4 ) и автоматизированные доказательные устройства теорем (ATP) на основе резолюций , включая E , SPASS и Vampire ( метод доказательства Metis [b] реконструирует доказательства резолюций, сгенерированные этими ATP). [4] Он также предлагает два поисковика моделей ( генератора контрпримеров ): Nitpick [5] и Nunchaku . [6]

Isabelle предлагает локали, которые являются модулями, структурирующими большие доказательства. Локаль фиксирует типы, константы и предположения в указанной области действия [5], так что их не нужно повторять для каждой леммы .

Isar (« понятное полуавтоматическое рассуждение ») — формальный язык доказательств Изабель. Он вдохновлен системой Mizar . [5]

Пример доказательства

Isabelle позволяет писать доказательства в двух разных стилях: процедурном и декларативном . Процедурные доказательства определяют ряд тактик ( функций/процедур доказательства теорем ), которые следует применять. Хотя они отражают процедуру, которую математик-человек может применить для доказательства результата, их обычно трудно читать, поскольку они не описывают результат этих шагов. Декларативные доказательства (поддерживаемые языком доказательств Isabelle, Isar), с другой стороны, определяют фактические математические операции, которые необходимо выполнить, и поэтому их легче читать и проверять людям.

Процедурный стиль устарел в последних версиях Isabelle. [ необходима ссылка ]

Например, декларативное доказательство от противного в языке Изар того, что квадратный корень из двух не является рациональным числом, можно записать следующим образом.

теорема sqrt2_not_rational: "sqrt 2 ∉ ℚ" доказательство пусть ?x = "sqrt 2" предположим "?x ∈ ℚ" тогда получим mn :: nat где sqrt_rat: "¦?x¦ = m / n" и lower_terms: "взаимно простое m n" по (правило 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 m n" по (правило gcd_greatest) с lower_terms имеем "2 dvd 1" по simp таким образом False используя odd_one по blast qed

Приложения

Isabelle использовался для поддержки формальных методов спецификации, разработки и проверки программных и аппаратных систем.

Изабель использовалась для формализации многочисленных теорем из математики и компьютерных наук , таких как теорема Гёделя о полноте , теорема Гёделя о непротиворечивости аксиомы выбора , теорема о простых числах , корректность протоколов безопасности и свойства семантики языков программирования . Многие из формальных доказательств, как уже упоминалось, поддерживаются в Архиве формальных доказательств, который содержит (по состоянию на 2019 год) не менее 500 статей с более чем 2 миллионами строк доказательств в общей сложности. [7]

  • В 2009 году проект L4.verified в NICTA представил первое формальное доказательство функциональной корректности ядра операционной системы общего назначения: [8] микроядро seL4 (secure embedded L4 ) . Доказательство построено и проверено в Isabelle/HOL и включает в себя более 200 000 строк скрипта доказательства для проверки 7 500 строк C. Проверка охватывает код, дизайн и реализацию, а основная теорема гласит, что код C правильно реализует формальную спецификацию ядра. Доказательство выявило 144 ошибки в ранней версии кода C ядра seL4 и около 150 проблем в каждом из дизайна и спецификации.

Ларри Полсон ведет список исследовательских проектов, в которых используется Isabelle. [10]

Альтернативы

Несколько языков и систем предоставляют схожие функции:

Примечания

  1. ^ / ˌ ɪ z ə ˈ b ɛ l /
  2. ^ / ˈ m iː t ɪ s /

Ссылки

  1. ^ Paulson, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237–258. arXiv : cs/9301104 . doi :10.1016/0743-1066(86)90015-4. S2CID  27085090.
  2. ^ Эберл, Мануэль; Кляйн, Гервин; Нипков, Тобиас; Полсон, Ларри ; Тиманн, Рене. «Архив формальных доказательств» . Проверено 1 мая 2021 г.
  3. ^ Гордон, Майк (1994-11-16). "1.2 История". Изабель и Х.О.Л. Исследования Кембриджского AR (Группа автоматизированного рассуждения). Архивировано из оригинала 2017-03-05 . Получено 2016-04-28 .
  4. ^ Джасмин Кристиан Бланшетт, Лукас Бульван, Тобиас Нипков, «Автоматическое доказательство и опровержение в Isabelle/HOL», в: Чезаре Тинелли, Виорика Софрони-Стоккерманс (ред.), Международный симпозиум по границам комбинированных систем – FroCoS 2011, Springer, 2011.
  5. ^ abc Жасмин Кристиан Бланшетт, Матиас Флери, Питер Ламмих и Кристоф Вайденбах, «Проверенная структура решателя SAT с обучением, забыванием, перезапуском и инкрементностью», Журнал автоматизированного рассуждения 61 :333–365 (2018).
  6. ^ Эндрю Рейнольдс, Жасмин Кристиан Бланшетт, Саймон Круанес, Чезаре Тинелли, «Поиск моделей для рекурсивных функций в SMT», в: Никола Оливетти, Ашиш Тивари (ред.), 8-я Международная совместная конференция по автоматизированному рассуждению, Springer, 2016.
  7. ^ Эберл, Мануэль; Кляйн, Гервин; Нипков, Тобиас; Полсон, Ларри ; Тиманн, Рене. «Архив формальных доказательств» . Проверено 22 октября 2019 г.
  8. ^ Кляйн, Гервин; Элфинстоун, Кевин; Хейзер, Гернот; Андроник, Джун; Кок, Дэвид; Деррин, Филипп; Элкадуве, Дхаммика; Энгельхардт, Кай; Колански, Рафал; Норриш, Майкл; Сьюэлл, Томас; Тач, Харви; Уинвуд, Саймон (октябрь 2009 г.). "seL4: Формальная проверка ядра ОС" (PDF) . 22-й симпозиум ACM по принципам операционных систем . Биг Скай, Монтана, США. стр. 207–200.
  9. ^ Strniša, Rok; Parkinson, Matthew (7 февраля 2011 г.). "Lightweight Java". Архив формальных доказательств (редакция за февраль 2011 г.). ISSN  2150-914X . Получено 25.11.2019 .
  10. ^ «Проекты — Wiki сообщества Изабель».

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

  • Лоуренс К. Полсон , «Основание универсального средства доказательства теорем», Журнал автоматизированного рассуждения , том 5, выпуск 3 (сентябрь 1989 г.), страницы: 363–397, ISSN  0168-7433.
  • Лоуренс К. Полсон и Тобиас Нипков , «Учебное пособие и руководство пользователя Isabelle», 1990.
  • MA Ozols, KA Eastaughffe и A. Cant, "DOVE: инструмент для проектно-ориентированной проверки и оценки", Труды AMAST 97 , редактор M. Johnson, Сидней, Австралия. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
  • Тобиас Нипков, Лоуренс К. Полсон, Маркус Венцель, «Изабель/HOL – помощник доказательства для логики высшего порядка», 2020.
  • Официальный сайт
  • Изабель на Stack Overflow
  • Архив формальных доказательств
  • IsarMathLib
Взято с "https://en.wikipedia.org/w/index.php?title=Изабель_(помощник_доказательства)&oldid=1252907351"