Автоматическое доказательство

Системы доказательства теорем делятся на две группы:

Системы интерактивного поиска доказательства теорем (редакторы доказательств). Они позволяют пользователям конструировать доказательство под контролем системы.

Автоматические генераторы доказательств. В них пользователь только ставит задачу («необходимо доказать теорему»), после чего генератор работает до обнаружения доказательства или выполнения условия останова.

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

Некоторые системы интерактивного поиска доказательства теорем:

Coq. Предоставляет язык программирования и окружение для создания формальных доказательств. Позволяет пользователям записывать математические утверждения и применять логические правила для доказательства этих утверждений.

Isabelle. Предоставляет окружение для формализации и проверки доказательств. Использует логику второго порядка и предлагает различные инструменты для автоматического и интерактивного доказательства.

Есть еще ряд решений для интерактивного поиска доказательства теорем, которые используют Python или другой вид высокоуровневых языков, которые формируют интерефейс для системы автоматического доказательства теорем:

Knuckledragger - это инструмент интерактивного доказательства теорем на python с помощью уже существующих автоматизированных решателей.

Автоматизированные системы доказательства теорем

Некоторые автоматические генераторы доказательств:

Prover9. Основана на методе резолюций и может генерировать доказательства в логике первого порядка.

E. Cредство проверки теорем о насыщении для логики первого и более высокого порядка с равенством.

Z3. Это система доказательства теорем от Microsoft Research, получивший несколько наград и имеющий активное сообщество разработчиков с открытым исходным кодом. Предоставляет возможность генерации доказательств в различных формальных системах и языках программирования.

nanoCoP - это компактный неклаузальный автоматический инструмент для доказательства теорем классической логики первого порядка. Он основан на неклаузальном математическом анализе связей для классической логики. Более подробную информацию об этом методе можно найти в документации.

Twee - это инструмент для доказательства теорем в области эквациональной логики. Он использует в качестве входных данных два набора уравнений, аксиомы и гипотезы, и пытается доказать гипотезы, исходя из аксиом. Как получить копию, смотрите на странице установки; возможно, вы также захотите ознакомиться с кратким руководством.

cvc5 - это эффективный автоматический тестер теорем с открытым исходным кодом для задач теории выполнимости по модулю (SMT). Он может быть использован для доказательства выполнимости (или, как правило, достоверности) формул первого порядка относительно (комбинаций) различных полезных базовых теорий. Кроме того, он предоставляет механизм синтаксического синтеза (SyGuS) для синтеза функций с учетом базовых теорий и их комбинаций.

Yices 2 - это SMT-решатель, который определяет выполнимость формул, содержащих неинтерпретированные функциональные символы с равенством, действительную и целочисленную арифметику, битовые векторы, скалярные типы и кортежи. Yices 2 поддерживает как линейную, так и нелинейную арифметику.

OpenSMT - это компактный SMT-решатель с открытым исходным кодом, написанный на C++, основная цель которого - сделать SMT-решатели простыми для понимания и использования в качестве вычислительного механизма для формальной проверки. OpenSMT построен поверх MiniSat.

Mizar - The Mizar project started around 1973 as an attempt to reconstruct mathematical vernacular in a computer-oriented environment.

https://www.cs.ru.nl/~freek/mizar/ - станица с описанием языка Mizar

Языковые модели для доказательства теорем

Также существует языковая модель GPT-f, которую обучили генерировать доказательства теорем.

Библиотеки

SMT-LIB - это международная инициатива, направленная на содействие исследованиям и разработкам в области теорий выполнимости по модулю (SMT). С момента своего создания в 2003 году инициатива преследовала эти цели, сосредоточившись на следующих конкретных задачах: С момента своего создания в 2003 году инициатива преследовала эти цели, сосредоточившись на следующих конкретных задачах:

Предоставьте стандартные подробные описания базовых теорий, используемых в SMT-системах. Разработайте и продвигайте общие языки ввода и вывода для SMT-решателей. Объедините разработчиков, исследователей и пользователей SMT и создайте вокруг них сообщество. Создайте и предоставьте в распоряжение исследовательского сообщества большую библиотеку тестов для SMT-решателей. Собирать и продвигать программные средства, полезные для сообщества SMT.

Этот веб-сайт предоставляет доступ к следующим основным материалам инициативы.

Документы, описывающие язык ввода-вывода SMT-LIB для решателей SMT и его семантику; Спецификации базовых теорий и логики.; Большая библиотека входных задач, или тестов, написанных на языке SMT-LIB. Ссылки на SMT-решатели и связанные с ними инструменты и утилиты.

Mizar Mathematical Library

Музей систем доказательства теорем

Ещё можно заглянуть в музей систем доказательства теорем.

Литература

• A Comparison of Mizar and Isar
• Paulson, L.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer, 1994.
• Paulson, L. C.: Isabelle's logics: FOL and ZF, 2002b. http://isabelle.in.tum.de/doc/logics-ZF.pdf.
• Wenzel, M.: The Isabelle/Isar Reference Manual, TU München, 2002b. http://isabelle.in.tum.de/doc/isar-ref.pdf
• Wiedijk, F.: Mizar light for HOL light, in R. J. Boulton and P. B. Jackson (eds), Theorem Proving in Higher Order Logics: TPHOLs 2001, LNCS 2152, 2001.
• Интеллектуальные системы. Теория и приложения

---