Table of contents for the series on Knights, Knaves, and Normals puzzles

1. Limitations of propositional logic
   • In which we discuss why propositional logic is far from ideal when it comes to represent these puzzles formally
2. Predicates and quantifiers to the rescue
   • In which we discuss how to use first-order predicate calculus to represent succinctly the type constraints on all inhabitants
3. Representing statements made by islanders
   • In which we discuss how to use first-order predicate calculus to represent the fact a specific islander made a given statement
4. First puzzle, solved with Mace4
   • In which we discuss how to represent a full puzzle statement in first-order predicate logic and use Mace4 to automatically discover/prove the correct solution to this puzzle
5. First puzzle, solved with Prover9
   • In which we discuss how to represent our first puzzle correctly for input to Prover9 and then exhibit a formal proof of the correctness of our solution to this puzzle
6. Second puzzle, solved with Prover9
   • In which we discuss how to solve our second puzzle which asks for a proof of a given result and is thus a perfect fit for Prover9
7. Third puzzle, on the island of Bahava
   • In which we discuss how to solve our third puzzle, which takes place on the island of Bahava, where normals can only marry normals and knights can only marry knaves (and vice-versa)
8. Fourth puzzle, on the island of Bahava
   • In which we discuss how to solve our last puzzle, which takes place again on the island of Bahava, and involves two couples