Automatic theorem proving

Question

I'm looking for an automatic theorem proving system, which can prove this:

Crocodile took mans child. Man asked crocodile not to eat his child. But Crocodile said: I'll return your child to you, if you will tell me, what am I going to do with him.

Analytical solution to his looks like this:

x - crocodile will eat child y - men answers: crocodile will eat child

~ means equality, ! means not, -> implies, + OR;

((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;

So, the answers is that men has to say: "You are not going to eat the child";

Now, there are plenty of systems listed here: http://en.wikipedia.org/wiki/Automated_theorem_proving

I've tried 5-6 of them, but couldn't really understand what am I doing here. How to formalize this theorem inside them, so that I could enter this first part of it:

((x~y)->!x) and ((x XOR y)->x)

and get the answer

y as an output.

Can any once advice, which system at least capable of doing so automatically, and give me some more hints?

Regards, Konstantin.

Answer 1

Well, your question target it's a lot higher than usual, I don't understand sufficiently your task to help...

I just goggled 'tableaux in Prolog', and would suggest to try first the simpler one, before delving into something more sophisticated (but I don't even know if that kind of logic is appropriate for your task).

Answer 2

After lots of reserach, I actually found out there are many programs like this, so my answer is : yes, such theorem can be proved automatically. Online example: http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html