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
Automatic theorem proving
-
01-06-2022 - |
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.
Solution 2
OTHER TIPS
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).
Checkout prolog. It's great for logical propositions and that sort of thing. Start with a read through the wiki and see if it sounds like what you want. It is a logical programming language - it will help you to build your own theorem proving algorithms.
Wiki: http://en.wikipedia.org/wiki/Prolog
Tutorials: http://cs.union.edu/~striegnk/courses/esslli04prolog/index.php