Автоматическое доказательство: различия между версиями
Vserge (обсуждение | вклад) (Первая редакция страницы) |
Vserge (обсуждение | вклад) м (добавил разделитель сносок и основного текста) |
||
| Строка 18: | Строка 18: | ||
Также существует языковая модель [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], которую обучили генерировать доказательства теорем. |
||
| + | |||
| + | ---- |
||
Версия 20:25, 22 февраля 2025
Системы доказательства теорем делятся на две группы[1]:
Системы интерактивного поиска доказательства теорем (редакторы доказательств). Они позволяют пользователям конструировать доказательство под контролем системы.
Автоматические генераторы доказательств. В них пользователь только ставит задачу («необходимо доказать теорему»), после чего генератор работает до обнаружения доказательства или выполнения условия останова.
Некоторые системы интерактивного поиска доказательства теорем:
Coq. Предоставляет язык программирования и окружение для создания формальных доказательств. Позволяет пользователям записывать математические утверждения и применять логические правила для доказательства этих утверждений.
Isabelle. Предоставляет окружение для формализации и проверки доказательств. Использует логику второго порядка и предлагает различные инструменты для автоматического и интерактивного доказательства.
Некоторые автоматические генераторы доказательств:
Prover9. Основана на методе резолюций и может генерировать доказательства в логике первого порядка.
Z3. Предоставляет возможность генерации доказательств в различных формальных системах и языках программирования.
Также существует языковая модель GPT-f, которую обучили генерировать доказательства теорем.