Solving Knights and Knaves with Alloy

There’s a famous logic puzzle, originally from Raymond Smullyan, called a “Knights and Knaves” puzzle. We have a set of people, all of whom are either a Knight or a Knave. Knights only make true statements, and Knaves only make false statements. Usually the goal of the puzzle is to find out who is what. For example, if we have two people, A and B, and A says “both of us are knaves”, we know A is a knave and B is a knight....

Submit