Помощник по доказательствам

Интерактивный сеанс доказательства в CoqIDE, показывающий сценарий доказательства слева и состояние доказательства справа.

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

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

Сравнение систем [ править ]

Имя	Последняя версия	Разработчики)	Язык реализации	Функции
Имя	Последняя версия	Разработчики)	Язык реализации	Логика высшего порядка	Зависимые типы	Маленькое ядро	Автоматизация доказательства	Доказательство размышлением	Генерация кода
ACL2	8.3	Мэтт Кауфманн и Джей Стротер Мур	Общий Лисп	Нет	Нетипизированный	Нет	Да	Да ^[2]	Уже исполняемый файл
приглашенный	2.6.3	Ульф Норелл, Нильс Андерс Даниэльссон и Андреас Абель ( Чалмерс и Гетеборг )	Хаскелл	Да	Да	Да	Нет	Частичный	Уже исполняемый файл
Альбатрос	0.4	Хельмут Брандл	OCaml	Да	Нет	Да	Да	Unknown	Еще не реализовано
Кок	8.19.0	ИНРИА	OCaml	Да	Да	Да	Да	Да	Да
Ф*	репозиторий	Microsoft Research и INRIA	Ф*	Да	Да	Нет	Да	Да ^[3]	Да
ХОЛ Лайт	репозиторий	Джон Харрисон	OCaml	Да	Нет	Да	Да	Нет	Нет
HOL4	Кананаскис-13 (или репо)	Майкл Норриш, Конрад Слинд и другие.	Стандартный ML	Да	Нет	Да	Да	Нет	Да
Идрис	2 0.6.0.	Эдвин Брэди	Идрис	Да	Да	Да	Unknown	Частичный	Да
Изабель	Изабель2024 (май 2024 г.)	Ларри Полсон ( Кембридж ), Тобиас Нипков ( Мюнхен ) и Макариус Венцель	Стандартное машинное обучение , Scala	Да	Нет	Да	Да	Да	Да
Наклонять	v4.7.0 ^[4]	Леонардо де Моура ( Microsoft Research )	С++ , Бережливое производство	Да	Да	Да	Да	Да	Да
LEGO (не связано с Lego )	1.3.1	Рэнди Поллак ( Эдинбург )	Стандартный ML	Да	Да	Да	Нет	Нет	Нет
Метаматематика	v0.198 ^[5]	Норман Мегилл	АНСИ С
Плотник	8.1.11	Белостокский университет	Бесплатный Паскаль	Частичный	Да	Нет	Нет	Нет	Нет
Нктм
НуПРЛ	5	Cornell University	Общий Лисп	Да	Да	Да	Да	Unknown	Да
ПВС	6.0	НИИ Международный	Общий Лисп	Да	Да	Нет	Да	Нет	Unknown
Двенадцать	1.7.1	Франк Пфеннинг и Карстен Шюрманн	Стандартный ML	Да	Да	Unknown	Нет	Нет	Unknown

ACL2 - язык программирования, логическая теория первого порядка и средство доказательства теорем (как с интерактивным, так и с автоматическим режимами) в традиции Бойера-Мура.
Coq — позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации.
Средства доказательства теорем HOL — семейство инструментов, в конечном итоге созданное на основе средства доказательства теорем LCF . В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», гарантирующих логическую корректность. Составление стратегии дает пользователям возможность предоставлять важные доказательства при относительно небольшом количестве взаимодействий с системой. К членам семьи относятся:
- HOL4 – «Основной потомок», все еще находится в активной разработке. Поддержка московского ML и Poly/ML . Имеет лицензию в стиле BSD .
- HOL Light – процветающая «минималистская вилка». На основе OCaml .
- ProofPower – стал проприетарным, затем вернулся к открытому исходному коду. На основе стандарта ML .
IMPS, интерактивная система математических доказательств. ^[6]
Изабель — интерактивная программа для доказательства теорем, преемница HOL. Основная база кода имеет лицензию BSD, но дистрибутив Isabelle включает в себя множество дополнительных инструментов с разными лицензиями.
Jape – на основе Java.
Наклонять
КОНСТРУКТОР ЛЕГО
Матита – система освещения, основанная на исчислении индуктивных конструкций.
MINLOG – Помощник по доказательству, основанный на минимальной логике первого порядка.
Мицар – Помощник по доказательству, основанный на логике первого порядка в стиле естественной дедукции и теории множеств Тарского – Гротендика .
PhoX – Помощник по доказательству, основанный на расширяемой логике высшего порядка.
Система проверки прототипов (PVS) – язык доказательств и система, основанная на логике высшего порядка.
TPS и ETPS — интерактивные средства доказательства теорем, также основанные на простом лямбда-исчислении, но на независимой формулировке логической теории и независимой реализации.

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

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

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

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

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

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

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

Теорема	Помощник по доказательствам	Год
Теорема о четырех цветах ^[12]	Кок	2005
Теорема Фейта – Томпсона ^[13]	Кок	2012
Основная круга группа ^[14]	Кок	2013
Задача Эрдеша – Грэма ^[15]^[16]	Наклонять	2022
Полиномиальная гипотеза Фреймана-Рузы опровергнута $\mathbb {F} _{2}$ ^[17]	Наклонять	2023

См. также [ править ]

Автоматизированное доказательство теорем - область автоматизированных рассуждений и математической логики.
Компьютерное доказательство - математическое доказательство, хотя бы частично созданное компьютером.
Формальная проверка . Доказательство или опровержение правильности определенных предполагаемых алгоритмов.
Манифест QED - Предложение по созданию компьютерной базы данных всех математических знаний.
Теории выполнимости по модулю - Логическая проблема, изучаемая в информатике
Prover9 – автоматизированное средство доказательства теорем для логики первого порядка и эквациональной логики.

Примечания [ править ]

^ Орнес, Стивен (27 августа 2020 г.). «Журнал Quanta - Насколько близки компьютеры к автоматизации математических рассуждений?» .
^ Хант, Уоррен; Мэтт Кауфманн; Роберт Беллармин Круг; Дж. Мур; Эрик В. Смит (2005). «Мета-рассуждение в ACL2» (PDF) . Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 3603. стр. 163–178. дои : 10.1007/11541868_11 . ISBN 978-3-540-28372-0 .
^ Поиск «доказательств размышлением»: arXiv : 1803.06547
^ «Страница релизов Lean 4» . Гитхаб . Проверено 15 октября 2023 г.
^ «Выпуск v0.198 · метаматематика/Metamath-exe» . Гитхаб .
^ Фармер, Уильям М.; Гуттман, Джошуа Д.; Тайер, Ф. Хавьер (1993). «IMPS: интерактивная система математических доказательств» . Журнал автоматизированного рассуждения . 11 (2): 213–248. дои : 10.1007/BF00881906 . S2CID 3084322 . Проверено 22 января 2020 г.
^ https://github.com/coq-community/vscoq
^ Венцель, Макариус. «Изабель» . Проверено 2 ноября 2019 г.
^ «VS Code Lean 4» . Гитхаб . Проверено 15 октября 2023 г.
^ Видейк, Фрик (15 сентября 2023 г.). «Формализация 100 теорем» .
^ Геверс, Герман (февраль 2009 г.). «Помощники доказательства: история, идеи и будущее» . Садхана . 34 (1): 3–25. дои : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID 14827467 .
^ Гонтье, Жорж (2008), «Формальное доказательство — Теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11): 1382–1393, MR 2463991 , заархивировано (PDF) из оригинала в 2011 г. 08-05
^ «Фейт Томсон оказался в штабе Microsoft Research Inria Joint Center» . 19 ноября 2016 г. Архивировано из оригинала 19 ноября 2016 г. Проверено 7 декабря 2023 г.
^ Ликата, Дэниел Р.; Шульман, Майкл (2013). «Вычисление фундаментальной группы круга в гомотопической теории типов». 2013 28-й ежегодный симпозиум ACM/IEEE по логике в информатике . стр. 223–232. arXiv : 1301.3443 . дои : 10.1109/lics.2013.28 . ISBN 978-1-4799-0413-6 . S2CID 5661377 . Проверено 7 декабря 2023 г.
^ «Математическая задача, которую создавали 3500 лет, наконец получила решение» . IFLНаука . 11 марта 2022 г. Проверено 9 февраля 2024 г.
^ Авигад, Джереми (2023). «Математика и формальный поворот». arXiv : 2311.00007 [ math.HO ].
^ Сломан, Лейла (06 декабря 2023 г.). « Команда математики доказывает критическую связь между сложением и множествами» . Журнал Кванта . Проверено 7 декабря 2023 г.

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

Барендрегт, Хенк ; Геверс, Герман (2001). «18. Помощники по доказательству, использующие системы зависимых типов» (PDF) . В Робинсоне, Алан Дж.А.; Воронков, Андрей (ред.). Справочник по автоматизированному рассуждению . Том. 2. Эльзевир. стр. 1149–. ISBN 978-0-444-50812-6 . Архивировано из оригинала (PDF) 27 июля 2007 г.
Пфеннинг, Фрэнк . «17. Логические структуры» (PDF) . Справочник, том 2 , 2001 г. стр. 1065–1148.
Пфеннинг, Франк (1996). «Практика логических рамок». В Киршнер, Х. (ред.). Деревья в алгебре и программировании – CAAP '96 . Конспекты лекций по информатике. Том. 1059. Спрингер. стр. 119–134. дои : 10.1007/3-540-61064-2_33 . ISBN 3-540-61064-2 .
Констебль, Роберт Л. (1998). «X. Типы в информатике, философии и логике» . В Бассе, СР (ред.). Справочник по теории доказательств . Исследования по логике. Том. 137. Эльзевир. стр. 683–786. ISBN 978-0-08-053318-6 .
Видейк, Фрик (2005). «Семнадцать искателей мира» (PDF) . Университет Радбауд в Неймегене.

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

Музей доказательства теорем
«Введение» в сертифицированное программирование с зависимыми типами .
Введение в Coq Proof Assistant (с общим введением в интерактивное доказательство теорем)
Интерактивное доказательство теорем для пользователей Agda
Список инструментов для доказательства теорем

Каталоги

Цифровая математика по категориям: Доказатели тактики
Автоматизированные системы и группы дедукции
Доказательство теорем и автоматизированные системы рассуждений
База данных существующих систем механизированного мышления
NuPRL: Другие системы
«Конкретные логические структуры и реализации» . Архивировано из оригинала 10 апреля 2022 года . Проверено 15 февраля 2024 г. (Фрэнк Пфеннинг).
DMOZ : Наука: Математика: Логика и основы: Вычислительная логика: Логические структуры

[1] Орнес, Стивен (27 августа 2020 г.). «Журнал Quanta - Насколько близки компьютеры к автоматизации математических рассуждений?» .

[2] Хант, Уоррен; Мэтт Кауфманн; Роберт Беллармин Круг; Дж. Мур; Эрик В. Смит (2005). «Мета-рассуждение в ACL2» (PDF) . Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 3603. стр. 163–178. дои : 10.1007/11541868_11 . ISBN 978-3-540-28372-0 .

[3] Поиск «доказательств размышлением»: arXiv : 1803.06547

[4] «Страница релизов Lean 4» . Гитхаб . Проверено 15 октября 2023 г.

[5] «Выпуск v0.198 · метаматематика/Metamath-exe» . Гитхаб .

[6] Фармер, Уильям М.; Гуттман, Джошуа Д.; Тайер, Ф. Хавьер (1993). «IMPS: интерактивная система математических доказательств» . Журнал автоматизированного рассуждения . 11 (2): 213–248. дои : 10.1007/BF00881906 . S2CID 3084322 . Проверено 22 января 2020 г.

[7] ttps://github.com/coq-community/vscoq

[8] Венцель, Макариус. «Изабель» . Проверено 2 ноября 2019 г.

[9] «VS Code Lean 4» . Гитхаб . Проверено 15 октября 2023 г.

[10] Видейк, Фрик (15 сентября 2023 г.). «Формализация 100 теорем» .

[11] Геверс, Герман (февраль 2009 г.). «Помощники доказательства: история, идеи и будущее» . Садхана . 34 (1): 3–25. дои : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID 14827467 .

[12] Гонтье, Жорж (2008), «Формальное доказательство — Теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11): 1382–1393, MR 2463991 , заархивировано (PDF) из оригинала в 2011 г. 08-05

[13] «Фейт Томсон оказался в штабе Microsoft Research Inria Joint Center» . 19 ноября 2016 г. Архивировано из оригинала 19 ноября 2016 г. Проверено 7 декабря 2023 г.

[14] Ликата, Дэниел Р.; Шульман, Майкл (2013). «Вычисление фундаментальной группы круга в гомотопической теории типов». 2013 28-й ежегодный симпозиум ACM/IEEE по логике в информатике . стр. 223–232. arXiv : 1301.3443 . дои : 10.1109/lics.2013.28 . ISBN 978-1-4799-0413-6 . S2CID 5661377 . Проверено 7 декабря 2023 г.

[15] «Математическая задача, которую создавали 3500 лет, наконец получила решение» . IFLНаука . 11 марта 2022 г. Проверено 9 февраля 2024 г.

[16] Авигад, Джереми (2023). «Математика и формальный поворот». arXiv : 2311.00007 [ math.HO ].

[17] Сломан, Лейла (06 декабря 2023 г.). « Команда математики доказывает критическую связь между сложением и множествами» . Журнал Кванта . Проверено 7 декабря 2023 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]