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

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Интерактивная сессия в CoqIDE, на экране — текст доказательства слева и состояние доказательства справа.

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

Сравнение систем[править | править код]

Название Последняя версия Разработчик(и) Язык реализации Возможности
Логика высшего порядка Зависимые типы Маленькое ядро Автоматизация доказательств Proof by reflection Кодогенерация
ACL2[en] 8.2 Matt Kaufmann[en] и J Strother Moore[en] 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[en] в репозитории John Harrison OCaml Да Нет Да Да Нет Нет
HOL4[en] 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[en] (не связан с компанией LEGO) 1.3.1 Randy Pollack (Edinburgh) Standard ML Да Да Да Нет Нет Нет
Mizar[en] 8.1.05 Białystok University Free Pascal Частично Да Нет Нет Нет Нет
NuPRL[en] 5 Cornell University Common Lisp Да Да Да Да Неизвестно Да
PVS[en] 6.0 SRI International Common Lisp Да Да Нет Да Нет Неизвестно
Twelf[en] 1.7.1 Frank Pfenning and Carsten Schürmann Standard ML Да Да Неизвестно Нет Нет Неизвестно
  • HOL theorem prover — семейство программных продуктов, являющихся, в конечном итоге, производными от инструмента доказательства теорем LCF. Во всех этих системах логическим ядром является библиотека встроенного в них языка программирования. Теоремы представляют собой новые элементы языка и вводятся с использованием «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом количестве взаимодействий с системой. К этой группе систем относятся:
  • IMPS[4]

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

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

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

Примечания[править | править код]

  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.
  2. Поиск «proofs by reflection»: arXiv:1803.06547
  3. Lean Theorem Prover Releases page. GitHub.
  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.
  5. Wenzel, Makarius Isabelle.

Литература[править | править код]

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

Каталоги