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

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

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

Сравнение систем
НазваниеПоследняя версияРазработчик(и)Язык реализацииВозможности
Логика высшего порядкаЗависимые типыМаленькое ядроАвтоматизация доказательствProof by reflectionКодогенерация
ACL28.2Matt Kaufmann и J Strother MooreCommon LispНетнетипизированныйНетДаДа[1]генерирует исполняемый код
Agda2.6.0.1 Ulf Norell, Nils Anders Danielsson, и Andreas Abel (Технический университет Чалмерса и Гётеборгский университет)HaskellДаДаДаНетЧастичногенерирует исполняемый код
Albatross0.4 Helmut BrandlOCamlДаНетДаДаНеизвестноеще не реализовано
Coq8.11.0INRIAOCamlДаДаДаДаДаДа
F*в репозиторииMicrosoft Research и INRIAF*ДаДаНетДаДа[2]Да
HOL Lightв репозиторииJohn HarrisonOCamlДаНетДаДаНетНет
HOL4Kananaskis-12 (или в репозитории)Michael Norrish, Konrad Slind, and othersStandard MLДаНетДаДаНетДа
Isabelle2019Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius WenzelStandard ML, ScalaДаНетДаДаДаДа
Lean v3.4.2[3] Microsoft Research C++ Да Да Да Да Да Неизвестно
LEGO (не связан с компанией LEGO)1.3.1Randy Pollack (Edinburgh)Standard MLДаДаДаНетНетНет
Mizar8.1.05Białystok UniversityFree PascalЧастичноДаНетНетНетНет
NuPRL5Cornell UniversityCommon LispДаДаДаДаНеизвестноДа
PVS6.0SRI InternationalCommon LispДаДаНетДаНетНеизвестно
Twelf1.7.1Frank Pfenning and Carsten SchürmannStandard 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].

См. также

Примечания
  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.

Литература

Ссылки
Каталоги
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.