stringtranslate.com

Изабель (помощник по доказательству)

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

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

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

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

Функции

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

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

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

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

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

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

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

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

теорема sqrt2_not_rational: доказательство "sqrt 2 ∉ ℚ" пусть ?x = "sqrt 2" предположим, что "?x ∈ ℚ", затем получим mn :: nat где sqrt_rat: "¦?x¦ = m / n" и low_terms: "взаимнопростые m n " by (правило 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 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_greestest) с самые низкие_термы имеют «2 dvd 1» от simp, поэтому значение False при использовании нечетного_one от blast qed

Приложения

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

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

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

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

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

Примечания

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

Рекомендации

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

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

Внешние ссылки