Modelling Puzzles in First Order Logic

by Adrian Groza

Springer, 2021


This book provides a collection of logical puzzles modelled and solved in equational first order logic.
    The book can be seen both as an instrument to teach First Order Logic, and also as a recreational exercises. Yet, there is more to puzzles than recreation.
    The goal is to motivate students, and to increase their knowledge engineering skills by discussing a variety of puzzles and their formalisation in First Order Logic (FOL). One aim is to convince undergraduate students that formal reasoning and its technicalities (e.g. resolution, conjunctive normal form, Skolem functions, interpretation models, open world assumption) are not that scary. There is no need for the students to avoid logics and to migrate to the tribe of machine learning. Solving puzzles in first order logic can be an effective cognitive incentive to attract students to the knowledge representation and reasoning tribe.
    Instructors in computer science are aware of the cognitive value of modelling puzzles and developing problem-solving skills. Logical puzzles are an efficient pedagogical instrument to engage students in learning artificial intelligence. Various authors have argued on the benefits of puzzle-based learning from various perspectives: mind Danesi (2018a), pedagogical Meyer et al. (2014); Szeredi (2003), or anthropological Danesi (2018b). My objective throughout is to show how some of the puzzles in mathematical recreation domain can be modelled in first order logic.
    In most cases it is difficult to trace the origin of a puzzle. Some puzzles formalised here are taken or adapted from books, while others are taken from what we would call today mathematical brain teasers sites:,,,,,, The puzzle books that I used are: “The Lady or the Tiger? and Other Logic Puzzles” by Raymond Smullyan, Smullyan (2009), "What is the name of this book?, also by Smullyan, Smullyan (2011), “The Moscow Puzzles: 359 Mathematical Recreations” by Boris Kordemsky, Kordemsky (1992), “536 Puzzles and Curious Problems” by Henry Dudeney, Dudeney (2016), “The Colossal Book of Short Puzzles and Problems” by Martin Gardner, Gardner (2005), “Ahmes’ Legacy Puzzles and the Mathematical Mind” by Marcel Danesi, Danesi (2018a), “Math and Logic Puzzles for PC Enthusiasts” by J. Clessa, Clessa (1996), “The Riddle of Scheherazade and Other Amazing Puzzles Ancient and Modern” by Raymond Smullyan, Smullyan (1996), and “Introduction to Mathematical Logic” by Micha Walicki, Walicki (2016), "A style for typesetting logic puzzles" by Jesef Kleber, Kleber (2013), "Making Up Your Own Mind: Thinking Effectively Through Creative Puzzle-solving" by E. Burger, Burger (2018), "Metamagical Themes" by Douglas Hofstadter, Hofstadter (1985) or from the Golomb's book "Polyominoes: puzzles, patterns, problems, and packings", Golomb (1996). Instead of explaining the solution to the human agent, I focused on explaining how puzzles can be modelled in first order logic.
    To check each formalisation, I used two tools: Prover9 theorem prover and Mace4 model finder Mc-Cune et al. (2009). Some puzzles are easier to solve by the software agent (i.e. Prover9/Mace4), while others are easier for the human agent. One open question is: Which puzzle is easier to solve by the human agent and which by a software agent? For each puzzle, I present: i) its formalisation in FOL, ii) the models and proofs found by Mace4 or Prover9, and ii) a drawing of the puzzle. Each drawing benefits from some great L A TEXpackages like TikzPeople of Nils Fleischhacker Fleischhacker (2017), or the LogicPuzzle style of Josef Kleber, Kleber (2013).
    Puzzles are designed to test the ingenuity of humans Sutcliffe (2017). Thus, various books on solving puzzles provide hints and answers to the human agent. They aim to help either the learner to figure out the solution or to guide how to teach puzzle-based learning Meyer et al. (2014). Differently from these books, my objective is to help the human agent to model the puzzles in first order logic. Then, the software agent is responsible to find the solution. The solution found by the Prover9 Mace4 is then explained to the human agent. The reasoning steps of the resolution mechanism repre- sent the hints for a human agent how to find the solution himself. One advantage is that software agent is able to compute for the given puzzle not only one, but all solutions. After a modelling solution is found, most of the formalisations look simple. However, before a modelling solution is clarified, a complete and correct formalisation is not always easy to design. That’s because a small modelling error leads to wrong solutions or unsatisfiability. Yoda would say: “Hard to debug a FOL error is!”.
    The book starts with an introductory chapter for the tools of choice: Prover9 and Mace4. The more pressed reader, or those who are already familiar with Prover9 and Mace4, can skip this chapter and jump directly to Chapter 2. Then, there are 12 chapters, each containing 12 puzzles of increasing difficulty. By increasing the difficulty, the aim is to provide students with sufficient motivation to master the logical modeling patterns of FOL, but also to avoid the drudgery normally associated with drill exercises. Chapter 2 starts with micro-arithmetic puzzles that aim to accustom the reader with the syntax of Prover9 and Mace4. Chapter 3 formalises puzzles on number properties. Chapter 4 introduces some more practical quizzes like route finding, ambiguous dates, or Golomb ruler. Chapter 5 provides solutions for the twelve puzzles from the “world of ladies and tigers” created by Smullyan Smullyan (2009). Chapter 6 provides formalisations of the various popular Einstein or zebra puzzles. Chapter 7 takes the reader on a trip to the island of truth, an island also discovered by Smullyan Smullyan (2011). Here the knights are telling the truth while the knaves are telling lies. Chapter 8 collects puzzles related to interwoven family relationships, love and marriage. Chapter 9 models grid puzzles
starting with Latin or magic squares, and continuing with star battle puzzles or minesweeper. Chapter 10 takes the reader on a trip to Japan, by solving Sudoku-like puzzles: Killer Sudoku, Futoshiki, Kakurasu, Takuzo, Kakuro, or Kendoku. Chapter 11 continues the trip in Russia, by modelling the Moscow puzzles created by Kordemsky Kordemsky (1992). Chapter 12 introduces the square-world
of polyominoes, including tetrominoes, pentominoes Golomb (1996), or the broken chess puzzle of Dudeney Dudeney (2002). Chapter 13 formalises some self-referencing brain teasers.
    This book can be seen as an extension of the puzzle collection at the Thousands of Problems for Theorem Provers (TPTP) library Sutcliffe (2017). TPTP collection includes, among other problems, 138 puzzles. Here, I provide 144 newly formalised puzzles, with more focus on grid based puzzles, Sudoku-like puzzles, polyominoes, or combinatorial puzzles of Kordemsky Kordemsky (1992) or Dudeney Dudeney (2016). This book can be an instrument to teach logic at high school and under- graduate level. The puzzles here can be used as a warm-up and funny activity to start a lecture on first order logic and its friends.