I was looking at a 'knight and knave' problem from one of Smullyan's puzzle books and found this:

There are 3 persons: A,B,C

- At least one is a Knight.
- At least one is a Knave.
- One of them has a prize.
Each has a statement to say:

- A says: B doesn't have the prize
- B says: I don't have the prize
- C says: I have the prize
Who has the prize?

Would it be possible to solve this with coq?

What could be the goal? Goal is an assignment from {Knight, Knave} to variables A,B,C.

How can that even be stated?

(And how can we reduce this to SAT problem? Is that possible?)

I started like:

```
Inductive type : Set := K | V.
Inductive person : type -> Type :=
| Person: forall t:type, person t.
Axiom hasP: forall {t:type}, person t -> Prop.
Definition isK {t:type} (p:person t): Prop :=
match t with
| K => true
| _ => false
end = true.
Goal
exists (t1 t2 t3:type),
forall (a:person t1) (b:person t2) (c:person t3),
(t1=K \/ t2=K \/ t3=K) /\
(t1=V \/ t2=V \/ t3=V) /\
(hasP a \/ hasP b \/ hasP c) /\
(isK a -> ~hasP b) /\
(isK b -> ~hasP b) /\
(isK c -> hasP c).
```

`Inductive person := a | b | c.`

and `assignment : person -> type`

might be effective

Also: your formalization only requires knights to be honest. Are knaves not expected to lie?

Using person := a | b | c also lets you avoid forall. And since type is isomorphic to boolean, then that's basically already a SAT problem!

Last updated: Oct 04 2023 at 20:01 UTC