Smullyan-KnightsAndKnaves

Problems from raymond smullyans book 'What is the name of this book', the knights and knaves chapter.

Project Structure

There are three competing formalizations of knights and knaves.

Set Theory Approach

The setup for this approach is in settheory.lean.

This approach has many custom theorems(some used to solve puzzles and some not) concerning sets. You can forgo these and only have the basic setup.

Domain Specific Language(DSL) Approach

The setup for this approach is in dsl_knights_knaves.lean. You can read about this setup and solve problems here

Propositional Approach

This setup doesn't have its own file.

You just declare islanders say A,B,C as propositions:

A B C : Prop

and use the logic theorems available in lean.

You can read about this setup and solve problems here

How to solve any puzzle

You can take all cases of all islanders, then execute tauto which would break down the goal and fill truth values in the hypothesis and the goal. If the goal reduces to true, then you are done and if a hypothesis reduces to false then there was a contradiction and the goal can be closed. The way tauto actually works is a bit more complicated than that, you could also try simp [*] at * to use all simp lemmas on all hypothesis.

There are other provers that might be more suited for this however. You can look into:

• SMT solvers
• Prolog

Translation between puzzles

Puzzles can translated from one representation to the other, and the solution as well.

We have the following correspondence:

Note for ¬¬A, it is equivalent to A