Помощник по проверке

Программный инструмент, помогающий разрабатывать формальные доказательства посредством взаимодействия человека и машины.
Интерактивный сеанс проверки в CoqIDE, показывающий скрипт проверки слева и состояние проверки справа

В информатике и математической логике помощник по доказательству или интерактивный доказатель теорем — это программный инструмент, помогающий разрабатывать формальные доказательства с помощью человеко-машинного взаимодействия. Это включает в себя своего рода интерактивный редактор доказательств или другой интерфейс , с помощью которого человек может руководить поиском доказательств, детали которых хранятся в компьютере , а некоторые шаги предоставляются им .

Недавние усилия в этой области направлены на то, чтобы заставить эти инструменты использовать искусственный интеллект для автоматизации формализации обычной математики. [1]

Сравнение систем

ИмяПоследняя версияРазработчик(и)Язык реализацииФункции
Логика высшего порядкаЗависимые типыМаленькое ядроАвтоматизация доказательстваДоказательство путем размышленияГенерация кода
ACL28.3Мэтт Кауфманн и Джей Стротер МурОбщий ЛиспНетНетипизированныйНетДаДа [2]Уже исполняемый
Агда2.6.4.3 [3]Ульф Норелл, Нильс Андерс Даниэльссон и Андреас Абель ( Чалмерс и Гетеборг ) [3]Хаскелл [3]Да [ требуется ссылка ]Да [4]Да [ требуется ссылка ]Нет [ необходима ссылка ]Частично [ требуется ссылка ]Уже исполняемый [ требуется ссылка ]
Альбатрос0.4Хельмут БрандлOCamlДаНетДаДаНеизвестныйПока не реализовано
Кок8.20.0ИНРИЯOCamlДаДаДаДаДаДа
Ф*репозиторийMicrosoft Research и INRIAФ*ДаДаНетДаДа [5]Да
Хол-ЛайтрепозиторийДжон ХаррисонOCamlДаНетДаДаНетНет
ХОЛ4Кананаскис-13 (или репо)Майкл Норриш, Конрад Слинд и другиеСтандартный МЛДаНетДаДаНетДа
Идрис2 0.6.0.Эдвин БрэдиИдрисДаДаДаНеизвестныйЧастичныйДа
ИзабельIsabelle2024 (май 2024)Ларри Полсон ( Кембридж ), Тобиас Нипков ( Мюнхен ) и Макариус ВенцельСтандартный ML , ScalaДаНетДаДаДаДа
Наклонятьверсия 4.7.0 [6]Леонардо де Моура ( Microsoft Research )C++ , бережливыйДаДаДаДаДаДа
ЛЕГО1.3.1Рэнди Поллак ( Эдинбург )Стандартный МЛДаДаДаНетНетНет
Метаматv0.198 [7]Норман МегиллANSI C
Мицар8.1.11Белостокский университетБесплатный ПаскальЧастичныйДаНетНетНетНет
Нктм
НуПРЛ5Корнелльский университетОбщий ЛиспДаДаДаДаНеизвестныйДа
ПВС6.0SRI ИнтернешнлОбщий ЛиспДаДаНетДаНетНеизвестный
Двенадцать1.7.1Франк Пфеннинг и Карстен ШюрманнСтандартный МЛДаДаНеизвестныйНетНетНеизвестный
  • ACL2  — язык программирования, логическая теория первого порядка и средство доказательства теорем (как с интерактивным, так и с автоматическим режимами) в традиции Бойера–Мура.
  • Coq  – позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации.
  • HOL-доказательства теорем  – семейство инструментов, в конечном счете полученных из LCF-доказательства теорем . В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», которые гарантируют логическую корректность. Составление стратегий дает пользователям возможность создавать значимые доказательства с относительно небольшим количеством взаимодействий с системой. Члены семейства включают:
    • HOL4  – «основной потомок», все еще в стадии активной разработки. Поддержка как Moscow ML , так и Poly/ML . Имеет лицензию в стиле BSD .
    • HOL Light  – процветающий «минималистский форк». Основан на OCaml .
    • ProofPower – Был проприетарным, затем вернулся к открытому исходному коду. Основан на Standard ML .
  • IMPS, интерактивная система математических доказательств. [8]
  • Isabelle — интерактивный доказатель теорем, преемник HOL. Основная кодовая база лицензирована BSD, но дистрибутив Isabelle объединяет множество дополнительных инструментов с различными лицензиями.
  • Jape  – основан на Java.
  • Наклонять
  • ЛЕГО
  • Матита  – легкая система, основанная на исчислении индуктивных построений.
  • MINLOG  – Помощник доказательства, основанный на минимальной логике первого порядка.
  • Mizar  – помощник в доказательстве, основанный на логике первого порядка, в стиле естественной дедукции и теории множеств Тарского–Гротендика .
  • PhoX  – помощник по доказательству, основанный на логике высшего порядка, который является расширяемым.
  • Система проверки прототипов (PVS) – язык и система доказательств, основанные на логике высшего порядка.
  • TPS и ETPS – интерактивные средства доказательства теорем, также основанные на простом типизированном лямбда-исчислении, но основанные на независимой формулировке логической теории и независимой реализации.

Пользовательские интерфейсы

Популярным интерфейсом для помощников по проверке доказательств является Proof General на базе Emacs , разработанный в Эдинбургском университете .

Coq включает CoqIDE, основанный на OCaml/ Gtk . Isabelle включает Isabelle/jEdit, основанный на jEdit и инфраструктуре Isabelle/ Scala для обработки доказательств, ориентированных на документы. Совсем недавно были разработаны расширения Visual Studio Code для Coq, [9] Isabelle Макариусом Вензелем, [10] и для Lean 4 разработчиками leanprover. [11]

Степень формализации

Freek Wiedijk ведет рейтинг помощников по доказательству по количеству формализованных теорем из списка 100 известных теорем. По состоянию на сентябрь 2023 года только пять систем формализовали доказательства более 70% теорем, а именно Isabelle, HOL Light, Coq, Lean и Metamath. [12] [13]

Известные формализованные доказательства

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

ТеоремаПомощник по проверкеГод
Теорема о четырех красках [14]Кок2005
Теорема Фейта–Томпсона [15]Кок2012
Основная группа круга [16]Кок2013
Проблема Эрдеша – Грэма [17] [18]Наклонять2022
Полиномиальная гипотеза Фреймана-Ружи над [19] Ф 2 {\displaystyle \mathbb {F} _{2}} Наклонять2023
ББ(5) = 47 176 870 [20]Кок2024

Смотрите также

Примечания

  1. ^ Орнес, Стивен (27 августа 2020 г.). «Quanta Magazine – Насколько близки компьютеры к автоматизации математических рассуждений?».
  2. ^ Хант, Уоррен; Мэтт Кауфманн; Роберт Беллармин Круг; Дж. Мур; Эрик В. Смит (2005). "Мета-рассуждение в ACL2" (PDF) . Доказательство теорем в логике высшего порядка . Конспект лекций по информатике. Том 3603. С. 163–178. doi :10.1007/11541868_11. ISBN 978-3-540-28372-0.
  3. ^ abc "agda/agda: Agda — язык программирования с зависимой типизацией / интерактивное средство доказательства теорем". GitHub . Получено 31 июля 2024 г. .
  4. ^ "Агда Вики" . Проверено 31 июля 2024 г.
  5. ^ Поиск "доказательства путем отражения": arXiv :1803.06547
  6. ^ "Lean 4 Releases Page". GitHub . Получено 15 октября 2023 г.
  7. ^ "Выпуск v0.198 · ​​metamath/Metamath-exe". GitHub .
  8. ^ Фармер, Уильям М.; Гуттман, Джошуа Д.; Тайер, Ф. Хавьер (1993). «IMPS: интерактивная математическая система доказательства». Журнал автоматизированного рассуждения . 11 (2): 213–248. doi :10.1007/BF00881906. S2CID  3084322. Получено 22 января 2020 г.
  9. ^ "coq-community/vscoq". 29 июля 2024 г. – через GitHub.
  10. ^ Венцель, Макариус. "Изабель" . Получено 2 ноября 2019 г.
  11. ^ "VS Code Lean 4". GitHub . Получено 15 октября 2023 г. .
  12. Видейк, Фрик (15 сентября 2023 г.). «Формализация 100 теорем».
  13. Geuvers, Herman (февраль 2009 г.). «Proof assistants: History, ideas and future». Sādhanā . 34 (1): 3–25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID  14827467.
  14. ^ Гонтье, Жорж (2008), «Формальное доказательство — теорема о четырех цветах» (PDF) , Notices of the American Mathematical Society , 55 (11): 1382–1393, MR  2463991, архивировано (PDF) из оригинала 2011-08-05
  15. ^ "Feit thomson proof in coq - Microsoft Research Inria Joint Centre". 2016-11-19. Архивировано из оригинала 2016-11-19 . Получено 2023-12-07 .
  16. ^ Ликата, Дэниел Р.; Шульман, Майкл (2013). «Вычисление фундаментальной группы окружности в теории гомотопических типов». 2013 28-й ежегодный симпозиум ACM/IEEE по логике в компьютерных науках. стр. 223–232. arXiv : 1301.3443 . doi :10.1109/lics.2013.28. ISBN 978-1-4799-0413-6. S2CID  5661377 . Получено 2023-12-07 .
  17. ^ «Математическая задача, которая решалась 3500 лет, наконец-то получила решение». IFLScience . 2022-03-11 . Получено 2024-02-09 .
  18. ^ Авигад, Джереми (2023). «Математика и формальный поворот». arXiv : 2311.00007 [math.HO].
  19. ^ Сломан, Лейла (2023-12-06). «Команда математиков «А» доказывает критическую связь между сложением и множествами». Журнал Quanta . Получено 2023-12-07 .
  20. ^ "Мы доказали, что "BB(5) = 47,176,870"". The Busy Beaver Challenge . 2024-07-02 . Получено 2024-07-09 .

Ссылки

  • Барендрегт, Хенк ; Гейверс, Герман (2001). "18. Помощники доказательства, использующие системы зависимых типов" (PDF) . В Робинсоне, Алан JA; Воронков, Андрей (ред.). Справочник по автоматизированному рассуждению . Том 2. Elsevier. С. 1149–. ISBN 978-0-444-50812-6. Архивировано из оригинала (PDF) 27.07.2007.
  • Пфеннинг, Франк . "17. Логические структуры" (PDF) . Справочник, том 2, 2001. С. 1065–1148.
  • Пфеннинг, Франк (1996). «Практика логических структур». В Kirchner, H. (ред.). Деревья в алгебре и программировании – CAAP '96 . Конспект лекций по информатике. Том 1059. Springer. С. 119–134. doi :10.1007/3-540-61064-2_33. ISBN 3-540-61064-2.
  • Констебль, Роберт Л. (1998). "X. Типы в информатике, философии и логике". В Buss, SR (ред.). Справочник по теории доказательств . Исследования по логике. Т. 137. Elsevier. С. 683–786. ISBN 978-0-08-053318-6.
  • Видейк, Фрик (2005). «Семнадцать искателей мира» (PDF) . Университет Радбауд в Неймегене.
  • Музей Доказательства Теорем
  • «Введение» в сертифицированное программирование с зависимыми типами .
  • Введение в Coq Proof Assistant (с общим введением в интерактивное доказательство теорем)
  • Интерактивное доказательство теорем для пользователей Agda
  • Список инструментов доказательства теорем
Каталоги
  • Цифровая математика по категориям: Тактические доказательства
  • Автоматизированные системы и группы вычетов
  • Системы доказательства теорем и автоматизированного рассуждения
  • База данных существующих механизированных систем рассуждений
  • NuPRL: Другие системы
  • "Specific Logical Frameworks and Implementations". Архивировано из оригинала 10 апреля 2022 г. Получено 15 февраля 2024 г.(Франк Пфеннинг).
  • DMOZ : Наука: Математика: Логика и основы: Вычислительная логика: Логические структуры
Взято с "https://en.wikipedia.org/w/index.php?title=Proof_assistant&oldid=1250500502"