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

Интерактивная сессия в CoqIDE, на экране — текст доказательства слева и состояние доказательства справа.

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

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

Название	Последняя версия	Разработчик(и)	Язык реализации	Возможности
				Логика высшего порядка	Зависимые типы	Маленькое ядро	Автоматизация доказательств	Proof by reflection	Кодогенерация
ACL2^[англ.]	8.2	Matt Kaufmann^[англ.] и J Strother Moore^[англ.]	Common Lisp	Нет	нетипизированный	Нет	Да	Да[1]	генерирует исполняемый код
Agda	2.6.0.1	Ulf Norell, Nils Anders Danielsson, и Andreas Abel (Технический университет Чалмерса и Гётеборгский университет)	Haskell	Да	Да	Да	Нет	Частично	генерирует исполняемый код
Albatross	0.4	Helmut Brandl	OCaml	Да	Нет	Да	Да	Неизвестно	еще не реализовано
Coq	8.11.0	INRIA	OCaml	Да	Да	Да	Да	Да	Да
F*	в репозитории	Microsoft Research и INRIA	F*	Да	Да	Нет	Да	Да[2]	Да
HOL Light^[англ.]	в репозитории	John Harrison	OCaml	Да	Нет	Да	Да	Нет	Нет
HOL4^[англ.]	Kananaskis-12 (или в репозитории)	Michael Norrish, Konrad Slind, and others	Standard ML	Да	Нет	Да	Да	Нет	Да
Isabelle	2019	Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel	Standard ML, Scala	Да	Нет	Да	Да	Да	Да
Lean	v3.4.2[3]	Microsoft Research	C++	Да	Да	Да	Да	Да	Неизвестно
LEGO^[англ.] (не связан с компанией LEGO)	1.3.1	Randy Pollack (Edinburgh)	Standard ML	Да	Да	Да	Нет	Нет	Нет
Mizar^[англ.]	8.1.05	Białystok University	Free Pascal	Частично	Да	Нет	Нет	Нет	Нет
NuPRL^[англ.]	5	Cornell University	Common Lisp	Да	Да	Да	Да	Неизвестно	Да
PVS^[англ.]	6.0	SRI International	Common Lisp	Да	Да	Нет	Да	Нет	Неизвестно
Twelf^[англ.]	1.7.1	Frank Pfenning and Carsten Schürmann	Standard ML	Да	Да	Неизвестно	Нет	Нет	Неизвестно

• HOL theorem prover — семейство программных продуктов, являющихся, в конечном итоге, производными от инструмента доказательства теорем LCF. Во всех этих системах логическим ядром является библиотека встроенного в них языка программирования. Теоремы представляют собой новые элементы языка и вводятся с использованием «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом количестве взаимодействий с системой. К этой группе систем относятся:
  • HOL4
  • HOL Light
  • ProofPower
• IMPS^[4]

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

Популярным интерфейсом для инструментов интерактивного доказательства теорем является опирающийся на Emacs Proof General, разработанный в Эдинбургском университете. Coq включает в себя CoqIDE, который написан на OCaml/Gtk. В состав Isabelle входит Isabelle/jEdit, основанный на jEdit и инфраструктуре Isabelle/Scala для документо-ориентированной обработки доказательств. Для Visual Studio Code так же существует расширение, предназначенное для работы с Isabelle. Оно было разработано Makarius Wenzel^[5].

См. также

• Автоматическое доказательство
• Доказательные вычисления
• QED manifesto^[англ.]
• Формальная верификация
• Задача выполнимости формул в теориях
• Metamath — язык, предназначенный для разработки формальных математических утверждений, в экосистему которого входит инструмент интерактивного доказательства теорем и несколько баз данных с тысячами записанных и доказанных теорем.

Примечания

1. Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith. Meta Reasoning in ACL2 (англ.) // Springer Lecture Notes in Computer Science^[англ.] : journal. — 2005. — Vol. 3603. — P. 163—178. Архивировано 1 декабря 2021 года.
2. Поиск «proofs by reflection»: arXiv:1803.06547
3. Lean Theorem Prover Releases page  (неопр.). GitHub. Архивировано 5 сентября 2020 года.
4. Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: An interactive mathematical proof system (англ.) // Journal of Automated Reasoning^[англ.]. — 1993. — Vol. 11, no. 2. — P. 213—248. — doi:10.1007/BF00881906. Архивировано 4 июня 2020 года.
5. Wenzel, Makarius. Isabelle  (неопр.). Дата обращения: 31 мая 2020. Архивировано 4 июня 2020 года.

Литература

• Henk Barendregt and Herman Geuvers (2001). «Proof-assistants using Dependent Type Systems». В Handbook of Automated Reasoning.
• Frank Pfenning (2001). «Logical frameworks». В Handbook of Automated Reasoning.
• Frank Pfenning (1996). «The Practice of Logical Frameworks».
• Robert L. Constable (1998). «Types in computer science, philosophy and logic». В Handbook of Proof Theory.
• H. Geuvers. «Proof assistants: History, ideas and future».
• Freek Wiedijk. «The Seventeen Provers of the World»

Ссылки

• «Introduction» d Certified Programming with Dependent Types.
• Introduction to the Coq Proof Assistant (с общим введением в интерактивное доказательство теорем)
• Interactive Theorem Proving for Agda Users
• A list of theorem proving tools

Каталоги

• Digital Math by Category: Tactic Provers
• Automated Deduction Systems and Groups
• Theorem Proving and Automated Reasoning Systems
• Database of Existing Mechanized Reasoning Systems
• NuPRL: Other Systems
• Specific Logical Frameworks and Implementations
• DMOZ: Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks