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

Изабель
	Isabelle/jEdit работает на macOS
Оригинальный автор(ы)	Лоуренс Полсон
Разработчик(и)	Кембриджский университет и Мюнхенский технический университет и др.
Первоначальный выпуск	1986
Стабильная версия	Изабель2024 / май 2024 г .; 3 месяца назад
Написано в	Стандартное машинное обучение и Scala
Операционная система	Линукс , Виндовс , МакОС
Тип	Математика
Лицензия	Лицензия BSD
Веб-сайт	Изабель .в .цель .из

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

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

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

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

Функции

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

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

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

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

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

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

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

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

theorem sqrt2_not_rational:
  "sqrt 2 ∉ ℚ"
proof
  let ?x = "sqrt 2"
  assume "?x ∈ ℚ"
  then obtain m n :: nat where
    sqrt_rat: "¦?x¦ = m / n" and lowest_terms: "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "m^2 = ?x^2 * 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

Приложения

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

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

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

Определение языка программирования Lightweight Java было проверено на языке Изабель. ^[9]

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

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

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

Агда , написанная на Haskell
Coq , написанный на OCaml
Lean , написанный на C++
LEGO , написанный на стандартном ML штата Нью-Джерси.
Система Mizar , написанная на Free Pascal.
Метаматематика , написанная на ANSI C.
Prover9 , написанный на C , с графическим интерфейсом, написанным на Python.
Двенадцать , написанные на стандартном ML

Примечания

Ссылки

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

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

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

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

[2] / ˌ ɪ z ə ˈ b ɛ l /

[5] / ˈ m iː t ɪ s /

[1] Полсон, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237–258. arXiv : cs/9301104 . дои : 10.1016/0743-1066(86)90015-4 . S2CID 27085090 .

[3] Эберл, Мануэль; Кляйн, Гервин; Нипков, Тобиас; Полсон, Ларри; Тиманн, Рене. «Архив формальных доказательств» . Проверено 1 мая 2021 г.

[4] Гордон, Майк (16 ноября 1994 г.). «1.2 История» . Изабель и Хол . Кембриджские исследования AR (Группа автоматического рассуждения). Архивировано из оригинала 5 марта 2017 г. Проверено 28 апреля 2016 г.

[6] Жасмин Кристиан Бланшетт, Лукас Бульван, Тобиас Нипков, «Автоматическое доказательство и опровержение в Изабель/HOL» , в: Чезаре Тинелли, Виорика Софрони-Стоккерманс (ред.), Международный симпозиум по границам объединения систем - FroCoS 2011 , Springer, 2011 .

[:0-7] Перейти обратно: ^а ^б ^с Жасмин Кристиан Бланшетт, Матиас Флери, Питер Ламмих и Кристоф Вайденбах, «Проверенная структура решателя SAT с обучением, забыванием, перезапуском и приращением» , Journal of Automated Reasoning 61 : 333–365 (2018).

[8] Эндрю Рейнольдс, Жасмин Кристиан Бланшетт, Саймон Круанес, Чезаре Тинелли, «Поиск модели для рекурсивных функций в SMT» , в: Никола Оливетти, Ашиш Тивари (ред.), 8-я Международная совместная конференция по автоматизированному рассуждению , Springer, 2016.

[9] Эберл, Мануэль; Кляйн, Гервин; Нипков, Тобиас; Полсон, Ларри; Тиманн, Рене. «Архив формальных доказательств» . Проверено 22 октября 2019 г.

[Klein_EHACDEEKNSTW_09-10] Кляйн, Гервин; Эльфинстон, Кевин; Хейзер, Гернот; Андроник, июнь; Кок, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельхардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Тач, Харви; Уинвуд, Саймон (октябрь 2009 г.). «seL4: формальная проверка ядра ОС» (PDF) . 22-й симпозиум ACM по принципам работы операционных систем . Биг Скай, Монтана, США. стр. 207–200.

[11] Стрниша, Рок; Паркинсон, Мэтью (7 февраля 2011 г.). «Легкая Java» . Архив формальных доказательств (изд. февраля 2011 г.). ISSN 2150-914X . Проверено 25 ноября 2019 г.

[12] «Проекты — Wiki Сообщества Изабель» .

[1]

[а]

[2]

[3]

[б]

[4]

[5]

[6]

[7]

[8]

[9]

[10]