Главная
Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств. Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером.
Сравнение систем
- HOL theorem prover — семейство программных продуктов, являющихся, в конечном итоге, производными от инструмента доказательства теорем LCF. Во всех этих системах логическим ядром является библиотека встроенного в них языка программирования. Теоремы представляют собой новые элементы языка и вводятся с использованием «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом количестве взаимодействий с системой. К этой группе систем относятся:
- HOL4
- HOL Light
- ProofPower
- IMPS
Пользовательский интерфейс
Популярным интерфейсом для инструментов интерактивного доказательства теорем является опирающийся на Emacs Proof General, разработанный в Эдинбургском университете. Coq включает в себя CoqIDE, который написан на OCaml/Gtk. В состав Isabelle входит Isabelle/jEdit, основанный на jEdit и инфраструктуре Isabelle/Scala для документо-ориентированной обработки доказательств. Для Visual Studio Code так же существует расширение, предназначенное для работы с Isabelle. Оно было разработано Makarius Wenzel.