Автоматическое доказательство теорем
Я ищу автоматическую систему доказательства теорем, которая может доказать это:
Крокодил взял мужик ребенка. Человек попросил крокодила не есть его ребенка. Но Крокодил сказал: я верну тебе твоего ребенка, если ты скажешь мне, что я собираюсь делать с ним.
Аналитическое решение его выглядит так:
x - крокодил будет есть ребенка y - мужчины отвечают: крокодил будет есть ребенка
~ означает равенство,! означает нет, -> подразумевает, + ИЛИ;
((x~y)->!x) and ((x XOR y)->x) =
(x! and y +!x and y+!x)(!x!y+x and y+x) =
(!x+!y)(x+!y) = !y;
Итак, ответы таковы, что мужчины должны сказать: "Вы не собираетесь есть ребенка";
Теперь есть много систем, перечисленных здесь: http://en.wikipedia.org/wiki/Automated_theorem_proving
Я попробовал 5-6 из них, но не мог понять, что я здесь делаю. Как формализовать эту теорему внутри них, чтобы я мог ввести эту первую часть:
((x~y)->!x) and ((x XOR y)->x)
и получить ответ
y
в качестве выхода.
Может ли кто-нибудь когда-нибудь посоветовать, какая система хотя бы способна сделать это автоматически, и дать мне еще несколько советов?
С уважением, Константин.
3 ответа
После многих исследований я действительно обнаружил, что существует множество подобных программ, поэтому я отвечаю: да, такая теорема может быть доказана автоматически. Пример в сети: http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html
Ну, ваш целевой вопрос намного выше, чем обычно, я не понимаю вашу задачу, чтобы помочь...
Я просто поглядел на "tableaux in Prolog" и предложил бы сначала попробовать более простой, прежде чем углубляться во что-то более сложное (но я даже не знаю, подходит ли такая логика для вашей задачи).
Оформить заказ пролог. Это отлично подходит для логических предложений и тому подобное. Начните с чтения вики и посмотрите, звучит ли это так, как вы хотите. Это логический язык программирования - он поможет вам создать собственные алгоритмы доказательства теорем.
Вики: http://en.wikipedia.org/wiki/Prolog
Учебники: http://cs.union.edu/~striegnk/courses/esslli04prolog/index.php