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

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

• ACL2— язык программирования, логическая теория первого порядка и средство доказательства теорем (как с интерактивным, так и с автоматическим режимами) в традиции Бойера–Мура.
• 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.
• IMPS: An interactive mathematical proof system интерактивная система математических доказательств.^[4]
• Isabelle — интерактивный доказатель теорем, преемник HOL. Основная кодовая база лицензирована BSD, но дистрибутив Isabelle объединяет множество дополнительных инструментов с различными лицензиями.
• Jape – основан на Java.
• Lean
• LEGO (не связан с компанией LEGO)
• Matita – легкая система, основанная на исчислении индуктивных построений.
• MINLOG – Помощник доказательства, основанный на минимальной логике первого порядка.
• Nqthm
• Mizar – помощник в доказательстве, основанный на логике первого порядка, в стиле естественной дедукции и теории множеств Тарского–Гротендика .
• PhoX – помощник по доказательству, основанный на логике высшего порядка, который является расширяемым.
• PVS – язык и система доказательств, основанные на логике высшего порядка.
• TPS and ETPS – интерактивные средства доказательства теорем, также основанные на простом типизированном лямбда-исчислении, но основанные на независимой формулировке логической теории и независимой реализации.

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

• Автоматическое доказательство
• Доказательные вычисления
• QED manifesto
• Формальная верификация
• Задача выполнимости формул в теориях
• 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