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

In the previous post, we used Mace4 to solve the following puzzle:

We are given three people, A, B, C, one of whom is a knight, one a knave, and one normal (but not necessarily in that order). They make the following statements:

A: I am normal.

B: That is true. 

C: I am not normal. 

What are A, B, and C?

In this post, we use Prover9 to build a proof by contradiction of this puzzle's solution.

Here is the input that we fed to Mace4 to represent this puzzle:

in which:

• the first group of formulas represent the fact that each islander has EXACTLY (i.e., at least and at most) one of three types (knight, knave, or normal),
• the second group of formulas represent (to some extent; see below for details) the fact that the three islanders all have different types,
• the third group (of one formula) represents the fact that the three constants \(A\), \(B\), and \(C\) refer to three different islanders, and
• the last group of formulas represent the three statements made by the islanders.

Now, in addition to these formulas, we need to feed to Prover9 the goal that we are trying to prove, namely the solution of the puzzle:

\(Kna(A)\ \&\ Nor(B)\ \&\ Kni(C)\).

Unfortunately, given this input, Prover9 returns:

which means that Prover9 was not able to find a proof.

Why is Prover9 failing to find a proof for a solution that Mace4 found?

Was Mace4 wrong? Or is Prover9 less powerful than Mace4?

No! In this case, the problem lies somewhere else: Mace4 is using a piece of information that Prover9 does not have, namely the number of islanders that are relevant to this puzzle.

When using Mace4, recall that I set its domain_size parameter to 3. This is because the "domain" of a model in this case is the set of islanders involved in the puzzle.

This piece of information is important to the puzzle but is not encoded in the input we fed to Prover9.

The input we fed to Mace4 was augmented by the domain size parameter, which was NOT part of the input formulas. This extra parameter (or option) is not available to Prover9, which does not have an explicit domain (recall that it finds proofs instead of models).

Note that the formulas that form the second group we fed as input to Mace4, namely:

(exists x Kni(x)).
(exists x Kna(x)).
(exists x Nor(x)).

represent the fact that there exists at least one inhabitant of each type. But, while we know those to be A, B, and, C, the formulas do not imply that. That is because there could be additional inhabitants (other than A, B, and C) in the domain of discourse (i.e., the puzzle). 

What we need to do is to encode this information explicitly in the input we feed to Prover9.

This is actually easy; and there are several ways to do it. I chose to add the following formula to our puzzle description:

\(∀x\ (x\ =\ A\ |\ x\ =\ B\ |\ x\ =\ C)\)

which represents the fact that, if you randomly pick any islander, it will always end up being one element of the set {A, B, C}. 

In other words, the puzzle only involves these three inhabitants. Recall that we already encoded the fact that these three constants identify three distinct inhabitants.

The Prover9 syntax for this formula is:

forall x (x = A | x = B | x = C).

or simply:

x = A | x = B | x = C.

since each variable (e.g., x) is implicitly universally quantified.

Now, before we test Prover9 again, let me simplify our input a bit.

Look back at the first group of formulas  (in the image above, right below the puzzle statement) we fed to Mace4.

The last three formulas in this group represent the fact that no islander can have more than one type. For example, the formula:

Kni(x) -> (-Kna(x) & -Nor(x)).

means that any knight cannot be a knave nor a normal. Together, the three formulas in this group cover all possibilities.

However, this constraint can also be conveyed with the statement: 

"No inhabitant can be 

both a knight and a knave, 

nor both a knight and a normal, 

nor both a knave and a normal." 

which, in Prover9 notation, becomes:

-(Kni(x) & Kna(x)).

-(Kni(x) & Nor(x)).

-(Kna(x) & Nor(x)).

Since Prover9 will convert these three formulas to clauses, we might as well do it ourselves, yielding:

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

by De Morgan's law for distributing negation over conjunction.

So, here is our final input for Prover9:

And here is Prover9's output:

============================== PROOF =================================
1 (exists x Kni(x)) # label(non_clause).  [assumption].
2 (exists x Kna(x)) # label(non_clause).  [assumption].
3 (exists x Nor(x)) # label(non_clause).  [assumption].
4 Kni(B) & Nor(A) | Kna(B) & -Nor(A) | Nor(B) # label(non_clause).  [assumption].
5 Kna(A) & Nor(B) & Kni(C) # label(non_clause) # label(goal).  [goal].
7 -Kni(x) | -Kna(x).  [assumption].
8 -Kni(x) | -Nor(x).  [assumption].
9 -Kna(x) | -Nor(x).  [assumption].
10 x = A | x = B | x = C.  [assumption].
11 A = x | B = x | C = x.  [copy(10),flip(a),flip(b),flip(c)].
17 Kni(c1).  [clausify(1)].
18 Kna(c2).  [clausify(2)].
19 Nor(c3).  [clausify(3)].
20 Kna(A) | Nor(A).  [assumption].
21 Kni(B) | -Nor(A) | Nor(B).  [clausify(4)].
22 Nor(A) | Kna(B) | Nor(B).  [clausify(4)].
23 Kni(C) | Nor(C).  [assumption].
24 -Kna(A) | -Nor(B) | -Kni(C).  [deny(5)].
26 -Nor(c1).  [resolve(17,a,8,a)].
27 -Kna(c1).  [resolve(17,a,7,a)].
28 c1 = A | c1 = B | Kni(C).  [para(11(c,2),17(a,1)),flip(a),flip(b)].
29 -Nor(c2).  [resolve(18,a,9,a)].
30 -Kni(c2).  [ur(7,b,18,a)].
31 c2 = A | c2 = B | Kna(C).  [para(11(c,2),18(a,1)),flip(a),flip(b)].
34 c3 = A | c3 = B | Nor(C).  [para(11(c,2),19(a,1)),flip(a),flip(b)].
35 -Nor(A) | Nor(B) | -Kna(B).  [resolve(21,a,7,a)].
36 Nor(C) | -Kna(C).  [resolve(23,a,7,a)].
66 c2 = A | c2 = B | -Nor(C).  [para(11(c,2),29(a,1)),flip(a),flip(b)].
76 c1 = A | c1 = B | -Kna(A) | -Nor(B).  [resolve(28,c,24,c)].
83 c2 = A | c2 = B | Nor(C).  [resolve(31,c,36,b)].
86 c1 = A | c1 = B | c3 = A | c3 = B.  [hyper(8,a,28,c,b,34,c)].
89 c2 = A | c2 = B.  [resolve(83,c,66,c),merge(c),merge(d)].
90 c2 = B | Kna(A).  [para(89(a,1),18(a,1))].
93 c2 = B | -Nor(A).  [para(89(a,1),29(a,1))].
104 c1 = A | c1 = B | -Nor(B) | c2 = B.  [resolve(76,c,90,b)].
109 c1 = A | c1 = B | c3 = B | Nor(A).  [para(86(c,1),19(a,1))].
120 c1 = A | c1 = B | c3 = B | c2 = B.  [resolve(109,d,93,b)].
129 c1 = A | c1 = B | c2 = B | Nor(B).  [para(120(c,1),19(a,1))].
133 c1 = A | c1 = B | c2 = B.  [resolve(129,d,104,c),merge(d),merge(e),merge(f)].
134 c1 = A | c1 = B | Kna(B).  [para(133(c,1),18(a,1))].
135 c1 = A | c1 = B | -Nor(B).  [para(133(c,1),29(a,1))].
138 Nor(B) | c1 = A | c1 = B | c3 = B.  [hyper(35,a,109,d,c,134,c),merge(e),merge(f)].
149 c1 = A | c1 = B | c3 = B.  [resolve(138,a,135,c),merge(d),merge(e)].
150 c1 = A | c1 = B | Nor(B).  [para(149(c,1),19(a,1))].
152 c1 = A | c1 = B.  [resolve(150,c,135,c),merge(c),merge(d)].
153 c1 = B | Kni(A).  [para(152(a,1),17(a,1))].
156 c1 = B | -Nor(A).  [para(152(a,1),26(a,1))].
160 c1 = B | Nor(A).  [hyper(7,a,153,b,b,20,a)].
168 c1 = B.  [resolve(160,b,156,b),merge(b)].
169 -Kna(B).  [back_rewrite(27),rewrite([168(1)])].
170 -Nor(B).  [back_rewrite(26),rewrite([168(1)])].
171 Kni(B).  [back_rewrite(17),rewrite([168(1)])].
172 Nor(A).  [back_unit_del(22),unit_del(b,169),unit_del(c,170)].
173 c2 = B.  [back_unit_del(93),unit_del(b,172)].
174 $F.  [back_rewrite(30),rewrite([173(1)]),unit_del(a,171)].
============================== end of proof ==========================

It is the longest proof we have seen so far, no doubt!

But it was easy to produce (just one click!) once we had the correct logical formulation.

Can you make sense of (parts of) it? 

Can you relate (parts of) it to your informal proof? 

Or to the one that Raymond Smullyan provides on page 32 of the 2011 paperback Dover Recreational Math edition [ISBN: 9780486481982] of his 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles"?