[Part 6] Raymond Smullyan's Knights, Knaves, and Normals puzzles Second puzzle, solved with Prover9

For our second example, we will use the \(40^{th}\) puzzle in Chapter 3 of Raymond Smullyan's 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles". As stated on page 24 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

Here is an unusual one: Two people, A and B, each of whom is either a knight, or knave, or a normal, make the following statements:

A: B is a knight.

B: A is not a knight.  

Prove that at least one of them is telling the truth, but is not a knight.

One reason this puzzle is unusual is because the author gives us its solution and asks us to prove it.

This is a perfect fit for this series!

The author's proof appears on page 33. But we will use Prover9 to find one for us.

First, we represent our island's world in which each inhabitant has exactly one of three types, using our usual formulas:

Kni(x) | Kna(x) | Nor(x).
-Kni(x) | -Kna(x).
-Kni(x) | -Nor(x).
-Kna(x) | -Nor(x).

Second, we apply our representation principle to reflect the islanders' statements, namely:

---

 Representation principle for Knights, Knaves, and Normals puzzles

For any person P living on this island and any statement S
(with P represented by constant \(P\) 
and S represented by formula \(\varphi\)),
the fact that P said S
will be represented by the formula:

\((Kni(P)\ \&\ \varphi)\ |\ (Kna(P)\ \&\ {-\varphi})\ |\ Nor(P)\)

---

Collecting all of the formulas we need according to the discussion above, we get the following input to feed to Mace4:

The output generated by Mace4 is the following:

Even though I tried to translate this proof back into English, to be compared with my own proof, or Smullyan's, I was not really successful. 

I think that one difficulty is that informal proofs do not use anything like big disjunctions. But that is what Prover9 does, since it converts all formulas to clauses.

Maybe we'll have a chance to get back to this issue later on.