Инструмент интерактивного доказательства теорем
Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств. Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером.
Сравнение систем
| Название | Последняя версия | Разработчик(и) | Язык реализации | Возможности | |||||
|---|---|---|---|---|---|---|---|---|---|
| Логика высшего порядка | Зависимые типы | Маленькое ядро | Автоматизация доказательств | Proof by reflection | Кодогенерация | ||||
| ACL2[англ.] | 8.2 | Matt Kaufmann[англ.] и J Strother Moore[англ.] | 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[англ.] | в репозитории | John Harrison | OCaml | Да | Нет | Да | Да | Нет | Нет |
| HOL4[англ.] | 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[англ.] (не связан с компанией LEGO) | 1.3.1 | Randy Pollack (Edinburgh) | Standard ML | Да | Да | Да | Нет | Нет | Нет |
| Mizar[англ.] | 8.1.05 | Białystok University | Free Pascal | Частично | Да | Нет | Нет | Нет | Нет |
| NuPRL[англ.] | 5 | Cornell University | Common Lisp | Да | Да | Да | Да | Неизвестно | Да |
| PVS[англ.] | 6.0 | SRI International | Common Lisp | Да | Да | Нет | Да | Нет | Неизвестно |
| Twelf[англ.] | 1.7.1 | Frank Pfenning and Carsten Schürmann | Standard 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].
См. также
- Автоматическое доказательство
- Доказательные вычисления
- QED manifesto[англ.]
- Формальная верификация
- Задача выполнимости формул в теориях
- Metamath — язык, предназначенный для разработки формальных математических утверждений, в экосистему которого входит инструмент интерактивного доказательства теорем и несколько баз данных с тысячами записанных и доказанных теорем.
Примечания
- ↑ 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. Архивировано 1 декабря 2021 года.
- ↑ Поиск «proofs by reflection»: arXiv:1803.06547
- ↑ Lean Theorem Prover Releases page. GitHub. Архивировано 5 сентября 2020 года.
- ↑ 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. Архивировано 4 июня 2020 года.
- ↑ Wenzel, Makarius Isabelle. Дата обращения: 31 мая 2020. Архивировано 4 июня 2020 года.
Литература
- 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
