Table of contents for the series of posts on Knights and Knaves puzzles

1. Review of propositional logic
   • In which we discuss propositional variables, logical connectives, and a couple of logical equivalences
2. Representation principle for Knights and Knaves puzzles
   • In which we discuss a general principle for representing, in propositional logic, statements made by the island's inhabitants
3. First example - Informal solution
   • In which we discuss a typical puzzle with two inhabitants and solve it informally. A typical puzzle asks questions of the type: What is A?
4. First example - Formal proof
   • In which we discuss a complete, formal proof of the solution to our first puzzle
5. First example - A natural-deduction proof
   • In which we discuss what a natural-deduction-style proof looks like and provide such a formal proof by cases for our first example
6. First example - Truth table approach
   • In which we discuss how to solve a typical puzzle by building a truth table
7. First example - Proof by contradiction
   • In which we discuss an indirect proof of the puzzle's solution that contrasts with the direct proofs we gave earlier
8. Second example
   • In which we discuss both an informal solution and a formal, truth-table-based approach to a second typical puzzle with 3 inhabitants
9. Automating puzzle proofs with Prover9
   • In which we discuss an automatic theorem prover and use it to automatically generate a proof by contradiction of the solution to our first puzzle
10. Automating puzzle proofs with Mace4
    • In which we discuss how to automatically solve the first puzzle using another theorem prover that does not need the solution of the puzzle to generate the proof
11. Third example
    • In which we discuss how to solve a typical puzzle with more than one solution using both Prover9 and Mace4.
12. Fourth example
    • In which we discuss how to solve another typical problem that involves statements of the form "such and such inhabitants are (not) of the same type"
13. Fifth example
    • In which we discuss how to solve yet another type of puzzle that does not ask to determine the type of inhabitants but rather the answer that they will give to some question
14. Sixth example
    • In which we discuss how to solve yet another type of puzzle in which we have to use additional information given by the author, that is not part of the puzzle's storyline
15. Seventh example
    • In which we discuss how to solve yet another type of puzzle in which we must determine if the answers to two questions posed to two inhabitants are the same
16. Creating our own puzzle
    • In which we discuss how to reverse the truth-table approach to create new Knights and Knaves puzzles that are provably correct