Preface
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: www.brainzilla.com,
www.brainden.com, www.braingle.com,
www.geogebra.org, www.mathisfun.com, www.puzzlesite.nl,
www.popularmechanics.com. 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.
