I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover.
I'm having some problems formalizing this:
"John, Mary and Derek are three people. They work as cook, waiter or manager, but the order is unknown. John, a friend of Mary's brother, is younger than Mary. John's eyes are black. The waiter's eyes are blue. The manager has no brother or sister and he's the oldest. Use Otter to find the correct work of each one."
In particular, formalizing the younger-older relationship, I tried to write it like this:
But when I write it in otter, the solver starts to loop and never find the solution. Example:
set(auto). formula_list(usable). all x y (younger(x, y) & x != y <-> -younger(y, x)). younger(A, B). end_of_list.