## Three hats problem

There are three agents each wearing a red or blue hat, each agent can see the other hats but not his own. There is an announcement: "there are at most two blue hats" Does any agent now know the color of his own hat?

In general the answer is of course no. But what if there are indeed two blue hats, for example for agents 1 and 2?

If after the announcement none of the agents step forward we know that there were not two blue hats, so at most one hat is blue. This has become common knowledge

As the model shows if all agents have a red hat they will still not know the color of their hats. So, if after the second announcement no agent steps forward all agents wear a red hat. Since this has become common knowledge, of course the agents will know the colors of their hats.

## Test cases

Here are some examples of both true and false formulas. These are used as test cases for the program. Click on a formula to input it into the prover.

- K
_{1}M_{1}M_{3}K_{3}K_{2}K_{1}a → a - ¬(K
_{1}(a ∨ ¬b) ∧ M_{1}¬a ∧ M_{1}(¬a ∧ b)) - ¬M
_{1}(¬a ∧ a) - K
_{1}M_{1}M_{3}K_{3}K_{2}K_{3}a → M_{1}M_{3}a - ¬(K
_{1}(a ∨ b) ∧ M_{1}¬a ∧ M_{1}K_{1}M_{3}¬b ∧ (M_{1}K_{2}M_{1}(¬a ∧ ¬b) ∨ M_{1}(¬a ∧ ¬b) ∨ K_{1}a)) - ¬(K
_{1}M_{1}M_{3}K_{3}K_{2}K_{3}a ∧ K_{1}M_{3}M_{2}K_{3}M_{2}¬a) - ¬(K
_{1}M_{1}M_{3}K_{3}K_{2}K_{3}a ∧ K_{1}M_{3}K_{3}K_{2}(¬a ∨ x) ∧ K_{1}¬x) - K
_{1}(a → b) → ( K_{1}a → K_{1}b) - K
_{1}a → a - K
_{1}a → K_{1}K_{1}a - M
_{1}a → K_{1}M_{1}a - M
_{1}(K_{1}p ∨ M_{2}K_{2}K_{1}q) → K_{1}(¬q → p) - ((p ∧ ¬K
_{1}p) → ¬p) ∨ ((p ∧ ¬K_{1}p) → ¬((p ∧ ¬K_{1}p) → ¬K_{1}((p ∧ ¬K_{1}p) → p ))) - (K
_{1}(a ∨ b) ∧ (c → K_{1}¬b) ∧ (K_{1}a → d)) → (c → d) - (K
_{1}(g = K_{1}p) ∧ M_{1}g) → (g ∧ p) - (K
_{1}(g = K_{1}p) ∧ M_{1}¬g) → ¬g - (K
_{1}p ∧ K_{1}((a ∧ p) → b)) → K_{1}(a → b)

And here are some false formulas from the same source:

- (K
_{1}p ∧ K_{1}((a ∧ p) → b)) → (M_{1}¬b ∧ K_{1}(a → b)) - K
_{1}M_{1}M_{3}K_{3}K_{2}K_{3}a → b - ¬(K
_{1}(a ∨ ¬b) ∧ M_{1}¬a ∧ M_{1}b) - K
_{1}M_{1}M_{3}K_{3}K_{2}M_{3}a → K_{1}K_{3}a - ¬(K
_{1}(a ∨ b) ∧ M_{1}¬a ∧ (M_{1}(¬a ∧ ¬b) ∨ M_{1}a)) - ¬(K
_{1}M_{1}M_{3}K_{3}K_{2}K_{3}a ∧ K_{1}M_{3}K_{3}K_{2}(¬a ∨ x) ∧ ¬x) - ((p ∧ ¬K
_{1}p) → p) ∧ ((p ∧ ¬K_{1}p) → ¬((p ∧ ¬K_{1}p) → K_{1}((p ∧ ¬K_{1}p) → p ))) - ¬(K
_{1}M_{3}(M_{1}a ∨ K_{4}b) ∧ K_{3}(K_{1}K_{3}¬a ∧ M_{3}K_{4}K_{3}M_{6}¬b))