Автоматическое доказательство: различия между версиями
Vserge (обсуждение | вклад) (Добавлена информация про Knuckledragger) |
Vserge (обсуждение | вклад) м (Добавлены заголовки разделов) |
||
| Строка 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, которую обучили генерировать доказательства теорем.
Ещё можно заглянуть в музей систем доказательства теорем.