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

Материал из Свод знаний по информационному моделированию
Перейти к навигации Перейти к поиску
(Добавил ссылку на музей систем доказательства теорем)
м (Исправлена ссылка на музей систем доказательства теорем)
Строка 21: Строка 21:
 
Также существует языковая модель [https://neurohive.io/ru/papers/gpt-f-nejroset-generiruet-dokazatelstva-teorem/ GPT-f], которую обучили генерировать доказательства теорем.
 
Также существует языковая модель [https://neurohive.io/ru/papers/gpt-f-nejroset-generiruet-dokazatelstva-teorem/ GPT-f], которую обучили генерировать доказательства теорем.
   
Ещё можно заглянуть в [https://github.com/theoremprover-museum музей систем доказательства теорем].
+
Ещё можно заглянуть в [https://theoremprover-museum.github.io/ музей систем доказательства теорем].
   
 
----
 
----

Версия 20:43, 22 февраля 2025

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

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

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

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

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

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

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

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

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

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

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

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