Knights and Knaves are a variant of logic puzzles involving figuring out a solution to some logical constraints.
Is there a book which treats these issues formally, in detail? I am hoping it would formalize the notion of propositions, predicates and talk about second order logic (where knights and knaves start referring to their own statements) and possibly even deducing solutions with something like Prolog, or formalizing them in something like Coq