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

Question

Я ищу автоматическую систему доказательства теорем, которая может доказать это:

Крокодил взял мужик ребенка. Человек попросил крокодила не есть его ребенка. Но Крокодил сказал: я верну тебе твоего ребенка, если ты скажешь мне, что я собираюсь делать с ним.

Аналитическое решение его выглядит так:

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 в качестве выхода.

Может ли кто-нибудь когда-нибудь посоветовать, какая система хотя бы способна сделать это автоматически, и дать мне еще несколько советов?

С уважением, Константин.

Answer 1

После многих исследований я действительно обнаружил, что существует множество подобных программ, поэтому я отвечаю: да, такая теорема может быть доказана автоматически. Пример в сети: http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html

Answer 2

Ну, ваш целевой вопрос намного выше, чем обычно, я не понимаю вашу задачу, чтобы помочь...

Я просто поглядел на "tableaux in Prolog" и предложил бы сначала попробовать более простой, прежде чем углубляться во что-то более сложное (но я даже не знаю, подходит ли такая логика для вашей задачи).

Answer 3

Оформить заказ пролог. Это отлично подходит для логических предложений и тому подобное. Начните с чтения вики и посмотрите, звучит ли это так, как вы хотите. Это логический язык программирования - он поможет вам создать собственные алгоритмы доказательства теорем.

Вики: http://en.wikipedia.org/wiki/Prolog

Учебники: http://cs.union.edu/~striegnk/courses/esslli04prolog/index.php