Автоматическое доказательство: различия между версиями

Материал из Свод знаний по информационному моделированию
Перейти к навигации Перейти к поиску
(Добавлена информация про Knuckledragger)
м (Добавлены заголовки разделов)
Строка 4: Строка 4:
   
 
'''Автоматические генераторы доказательств.''' В них пользователь только ставит задачу («необходимо доказать теорему»), после чего генератор работает до обнаружения доказательства или выполнения условия останова.
 
'''Автоматические генераторы доказательств.''' В них пользователь только ставит задачу («необходимо доказать теорему»), после чего генератор работает до обнаружения доказательства или выполнения условия останова.
  +
  +
= Интерактивные системы доказательства теорем =
   
 
Некоторые системы интерактивного поиска доказательства теорем:
 
Некоторые системы интерактивного поиска доказательства теорем:
Строка 14: Строка 16:
   
 
[https://www.philipzucker.com/knuckledragger/ Knuckledragger] - это инструмент интерактивного доказательства теорем на python с помощью уже существующих автоматизированных решателей.
 
[https://www.philipzucker.com/knuckledragger/ Knuckledragger] - это инструмент интерактивного доказательства теорем на python с помощью уже существующих автоматизированных решателей.
  +
  +
= Автоматизированные системы доказательства теорем =
   
 
Некоторые автоматические генераторы доказательств:
 
Некоторые автоматические генераторы доказательств:

Версия 21:10, 22 февраля 2025

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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