Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Изабель
Изабель jedit.png
Isabelle / jEdit работает на macOS
Автор (ы) оригиналаЛоуренс Полсон
Разработчики)Кембриджский университет и Технический университет Мюнхена и др.
изначальный выпуск1986 [1]
Стабильный выпуск
Isabelle2020 / апрель 2020 года ; 11 мес. Назад ( 2020-04 )
Написано вСтандартный ML и Scala
Операционная системаLinux , Windows , Mac OS X
ТипМатематика
ЛицензияЛицензия BSD
Интернет сайтИзабель .in .tum .de

Изабель [а] автоматизированная теорема прувер является интерактивной теоремой прувер , А логика высшего порядка (HOL) теорема прувер . Это средство доказательства теорем в стиле LCF (написанное на стандартном языке ML ). Таким образом, он основан на небольшом логическом ядре (ядре) для повышения надежности доказательств, не требуя (но поддерживая) явные объекты доказательства.

Особенности [ править ]

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

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

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

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

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

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

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

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

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

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

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

теорема sqrt2_not_rational: "sqrt 2 ∉ ℚ" доказательство  let ? x = "sqrt 2"  принять  "? x ∈ ℚ",  затем  получить mn :: nat, где sqrt_rat: "¦? x¦ = m / n"  и lower_terms: " coprime mn " by (rule Rats_abs_nat_div_natE), следовательно,  " m ^ 2 =? x ^ 2 * n ^ 2 "  by (auto simp add: power2_eq_square), следовательно, eq: " m ^ 2 = 2 * n ^ 2 "  с использованием of_nat_eq_iff power2_eq_square , следовательно, fastforce " 2 DVD м ^ 2 " по simp отсюда  "2 dvd m" by simp иметь  доказательство "2 dvd n" - из ‹2 dvd m› получить k, где "m = 2 * k" .. с eq иметь "2 * n ^ 2 = 2 ^ 2 * k ^ 2" посредством simp, следовательно, " 2 DVD п ^ 2" по упр , таким образом , "2 DVD N" по Simp КЭД с <2 DVD м> есть "2 DVD НОД м н" по (правило gcd_greatest) с lowest_terms имеют "2 DVD 1"by simp, таким образом, False, используя                odd_one от blast qed

Приложения [ править ]

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

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

Ларри Полсон ведет список исследовательских проектов , в которых используется Изабель.

Альтернативы [ править ]

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

  • Coq , аналогичная система, написанная на OCaml
  • HOL , аналогично реализации HOL Изабель
  • Бережливая , похожая система, написанная на C ++
  • Система Мицар
  • Метамат
  • Доказатель9

Заметки [ править ]

  1. ^ / ˌ ɪ г ə б ɛ л /
  2. ^ / М я т ɪ с /

Ссылки [ править ]

  1. Перейти ↑ Paulson, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237. arXiv : cs / 9301104 . DOI : 10.1016 / 0743-1066 (86) 90015-4 .
  2. ^ Jasmin Кристиан Бланшетт, Lukas Bulwahn, Tobias Нипкова, "Автоматическое доказательство и Опровержение в Isabelle / HOL" , в: Чезаре Tinelli, Viorica Sofronie-Stokkermans (ред.), Международный симпозиум по Frontiers объединения систем - FroCoS 2011 , Springer, 2011 .
  3. ^ a b c Жасмин Кристиан Бланшетт, Матиас Флери, Питер Ламмих и Кристоф Вайденбах, «Проверенная структура SAT Solver с обучением, забыванием , перезапуском и инкрементностью» , Journal of Automated Reasoning 61 : 333–365 (2018).
  4. ^ Эндрю Рейнольдс, жасмин Кристиан Бланшетт, Саймон Cruanes, Чезаре Tinelli, "Модель Finding для рекурсивных функций в SMT" , в: Nicola Olivetti, Ashish Тивари (ред.), 8 - я Международная объединенная конференция по Automated Рассуждения , Springer, 2016.
  5. ^ Эберл, Мануэль; Кляйн, Гервин; Нипков, Тобиас; Полсон, Ларри; Тиманн, Рене. «Архив формальных доказательств» . Проверено 22 октября 2019 года .
  6. ^ Гордон, Майк (1994-11-16). «1.2 История» . Изабель и Хол . Кембриджские исследования AR (Группа автоматизированных рассуждений) . Проверено 28 апреля 2016 .
  7. ^ Кляйн, Гервин; Эльфинстон, Кевин; Хайзер, Гернот; Андроник, июнь; Петух, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельгардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Туч, Харви; Уинвуд, Саймон (октябрь 2009 г.). «seL4: Формальная проверка ядра ОС» (PDF) . 22-й симпозиум ACM по принципам операционных систем . Биг Скай, Монтана, США. С. 207–200.
  8. ^ Стрниша, Рок; Паркинсон, Мэтью (07.02.2011). «Легкая Java» . Архив формальных доказательств (ред., Февраль 2011 г.). ISSN 2150-914X . Проверено 25 ноября 2019 . 

Дальнейшее чтение [ править ]

  • Лоуренс К. Полсон , "Основы универсального средства доказательства теорем" , Журнал автоматизированного мышления , том 5, выпуск 3 (сентябрь 1989 г.), страницы: 363–397, ISSN 0168-7433 . 
  • Лоуренс С. Полсон и Тобиас Нипкоу , «Учебное пособие для Изабель и руководство пользователя» , 1990 г.
  • М.А. Озолс, К.А. Истофф и А. Кант, «DOVE: проверка и оценка , ориентированная на дизайн» , Труды AMAST 97 , М. Джонсон, редактор, Сидней, Австралия. Конспект лекций по информатике (LNCS) Vol. 1349, Springer Verlag, 1997.
  • Тобиас Нипкоу, Лоуренс С. Полсон, Маркус Венцель, «Изабель / HOL - помощник по проверке логики высокого порядка» , 2020.

Внешние ссылки [ править ]

  • Сайт Изабель
  • Изабель на Stack Overflow
  • Архив формальных доказательств
  • IsarMathLib