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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

---