On a certain island the inhabitants are partitioned into those who always tell t he
truth and those who always lie.
You land on the island and meet three inhabitants, A, B, and C.
You ask A, "Are you a truth-teller or a liar?"
He mumbles something that you cannot make out.
You ask B what A said.
B replies, "A said he is a liar".
C then volunteers, "Don't believe B, he's lying!"
Question: What can you tell about A, B, and C?
Solution: This puzzle has been solved.
We present the puzzle here as an example of some of the challenges one faces in representing implicit as well as explicit information to an automated reasoning program.
A detailed discussion of this puzzle and others is given in Automated Reasoning: Introduction and Applications, by Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. The book, published by McGraw-Hill, includes a diskette of the automated reasoning program OTTER, which can be used to solve puzzles as well as extremely challenging problems in mathematics and logic.
Those who have OTTER already may simply use the chosen clauses and start experimenting.