Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств. Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером.
Сравнение систем
Название Последняя версия Разработчик(и) Язык реализации Возможности Логика высшего порядка Зависимые типы Маленькое ядро Автоматизация доказательств Proof by reflection Кодогенерация 8.6 и Common Lisp Agda 2.6.2.2 Ulf Norell, Nils Anders Danielsson, и Andreas Abel (Технический университет Чалмерса и Гётеборгский университет) Haskell Albatross 0.4.4 Helmut Brandl OCaml еще не реализовано Rocq (ранее известный как Coq) 9.0.0 INRIA OCaml F* 0.9.6.0 Microsoft Research и INRIA F* Поиск «proofs by reflection»: в репозитории John Harrison OCaml HOL4 Kananaskis-12 (или в репозитории) Michael Norrish, Konrad Slind, and others Standard ML Idris 2 0.6.0 Edwin Brady Idris Isabelle Isabelle2021-1 Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel Standard ML, Scala Lean4.7.0 Microsoft Research C++ (не связан с компанией LEGO) 1.3.1 Randy Pollack (Edinburgh) Standard ML Mizar 8.1.05 Białystok University Free Pascal 5 Cornell University Common Lisp 6.0 SRI International Common Lisp 1.7.1 Frank Pfenning and Carsten Schürmann Standard ML
— язык программирования, логическая теория первого порядка и средство доказательства теорем (как с интерактивным, так и с автоматическим режимами) в традиции Бойера–Мура. Rocq (ранее известный как Coq) — позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации. HOL theorem prover – семейство программных продуктов, являющихся, в конечном итоге, производными от инструмента доказательства теорем LCF. Во всех этих системах логическим ядром является библиотека встроенного в них языка программирования. Теоремы представляют собой новые элементы языка и вводятся с использованием «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом количестве взаимодействий с системой. К этой группе систем относятся: HOL4 — единственная в настоящее время поддерживаемая и развиваемая система, происходящая от системы HOL88, которая была кульминацией первоначальных усилий по реализации HOL, возглавляемых Майком Гордоном . HOL88 включала собственную реализацию ML , которая, в свою очередь, была реализована поверх Common Lisp . Все системы, последовавшие за HOL88 (HOL90, hol98 и HOL4), были реализованы на Standard ML ; в то время как hol98 связан с Moscow ML , HOL4 может быть построен либо с Moscow ML, либо с Poly/ML . Все они поставляются с большими библиотеками кода доказательства теорем, которые реализуют дополнительную автоматизацию поверх очень простого основного кода. HOL Light — экспериментальная «минималистская» версия HOL, которая с тех пор выросла в другой основной вариант HOL; ее логические основы остаются необычайно простыми. HOL Light, изначально реализованный в Caml Light , теперь использует OCaml. ProofPower — набор из шести инструментов, разработанных для предоставления специальной поддержки, основанной на HOL, для работы с нотацией Z для формальной спецификации. Инструмент PPDaz, поддерживающий спецификацию и проверку программ, написанных на подмножестве Ada, ранее поставлялся только по проприетарной лицензии. HOL Zero — минималистская реализация, ориентированная на надежность. Candle — проверенная реализация HOL Light на основе CakeML. : An interactive mathematical proof system интерактивная система математических доказательств. Isabelle — интерактивный доказатель теорем, преемник HOL. Основная кодовая база лицензирована BSD, но дистрибутив Isabelle объединяет множество дополнительных инструментов с различными лицензиями. – основан на Java. Lean (не связан с компанией LEGO) – легкая система, основанная на исчислении индуктивных построений. – Помощник доказательства, основанный на минимальной логике первого порядка.
Mizar – помощник в доказательстве, основанный на логике первого порядка, в стиле естественной дедукции и теории множеств Тарского–Гротендика . – помощник по доказательству, основанный на логике высшего порядка, который является расширяемым. – язык и система доказательств, основанные на логике высшего порядка. and – интерактивные средства доказательства теорем, также основанные на простом типизированном лямбда-исчислении, но основанные на независимой формулировке логической теории и независимой реализации.
Пользовательский интерфейс Популярным интерфейсом для инструментов интерактивного доказательства теорем является опирающийся на 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). «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
Категория:Инструменты интерактивного доказательства теорем Категория:Автоматическое доказательство теорем