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

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

Название	Последняя версия	Разработчик(и)	Язык реализации	Возможности
				Логика высшего порядка	Зависимые типы	Маленькое ядро	Автоматизация доказательств		Кодогенерация
	8.2	и	Common Lisp	Нет	нетипизированный	Нет	Да	Да	генерирует исполняемый код
Agda	2.6.0.1	Ulf Norell, Nils Anders Danielsson, и Andreas Abel ( Технический университет Чалмерса и Гётеборгский университет )	Haskell	Да	Да	Да	Нет	Частично	генерирует исполняемый код
	0.4	Helmut Brandl	OCaml	Да	Нет	Да	Да	Неизвестно	еще не реализовано
Coq	8.11.0	INRIA	OCaml	Да	Да	Да	Да	Да	Да
F*	в репозитории	Microsoft Research и INRIA	F*	Да	Да	Нет	Да	Да	Да
	в репозитории	John Harrison	OCaml	Да	Нет	Да	Да	Нет	Нет
	Kananaskis-12 (или в репозитории)	Michael Norrish, Konrad Slind, and others	Standard ML	Да	Нет	Да	Да	Нет	Да
Isabelle	2019	( Cambridge ), ( München ) and	Standard ML , Scala	Да	Нет	Да	Да	Да	Да
Lean	v3.4.2	Microsoft Research	C++	Да	Да	Да	Да	Да	Неизвестно
(не связан с компанией LEGO)	1.3.1	( Edinburgh )	Standard ML	Да	Да	Да	Нет	Нет	Нет
	8.1.05		Free Pascal	Частично	Да	Нет	Нет	Нет	Нет
	5	Cornell University	Common Lisp	Да	Да	Да	Да	Неизвестно	Да
	6.0		Common Lisp	Да	Да	Нет	Да	Нет	Неизвестно
	1.7.1	and	Standard ML	Да	Да	Неизвестно	Нет	Нет	Неизвестно

• — семейство программных продуктов, являющихся, в конечном итоге, производными от инструмента доказательства теорем LCF . Во всех этих системах логическим ядром является библиотека встроенного в них языка программирования. Теоремы представляют собой новые элементы языка и вводятся с использованием «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом количестве взаимодействий с системой. К этой группе систем относятся:

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

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

См. также

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

Примечания

Литература

• Henk Barendregt and Herman Geuvers (2001). . В Handbook of Automated Reasoning .
• Frank Pfenning (2001). . В 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. « ».
• Freek Wiedijk. « »

Ссылки

• d Certified Programming with Dependent Types .
• (с общим введением в интерактивное доказательство теорем)

Каталоги

• DMOZ :