Modelling Puzzles in First Order Logic

Preface
Contents
1 Getting Started with Prover9 and Mace4
	1.1 Installing Prover9 and Mace4
	1.2 Finding Proofs
	1.3 Finding Models
	References
2 Micro-arithmetic Puzzles
	Logic equation 4x4
	Logic equation 4x4
	Logic equation 5x5
	Logic equation 9x9
	Three squares
	Pocket money
	Dividing the legacy
	Boys and girls
	Robinson's age
	Five cards
	A square family
	Family ages
	Reference
3 Strange Numbers
	Adding their cubes
	Multiplication
	The arithmetical cabby
	The ten barrels
	Find the triangle area
	A digital difficulty
	The archery match
	Target practice
	The nine barrels
	Upside-down year
	A twisted number
	Unusual number
	References
4 Practical Puzzles
	Secret letter to the parents
	Ambiguous dates
	One landlord and 100 servants
	Consecutive numbers
	Colouring Dracula's land in red
	Golomb ruler
	Two cube calendar
	How many routes?
	Going to church
	Buying wine
	Railway routes
	The stolen balsam
	References
5 Lady and Tigers
	Ladies and tigers
	Ladies and tigers reloaded
	Ladies only
	Ladies are honest but tigers are liars
	Ladies are honest in some rooms only
	The lady is on the other room
	Better choosing the other room
	Mixed messages on doors
	A lady and two tigers
	A lady and two tigers
	A lady, two tigers, and other messages
	A logic labyrinth
	References
6 Einstein Puzzles
	The magisterial bench
	Five ships in a port
	Ladies in the committee
	Cocktail party
	Borrowed books
	Baseball coach dilemma
	Perfect man
	Four bikers
	Movies night
	Secret Santa
	Seating the party
	Passengers in a railroad compartment
	References
7 Island of Truth
	We are both knaves
	At least one of us is a knave
	Either I am a knave or B is a knight
	We are both the same
	Three inhabitants and two messages
	Three inhabitants and not enough information
	Three inhabitants and two of the same type
	Jim, Jon, and Joe
	A spy appears
	Who is the spy?
	All truth and nothing but the truth
	Three goddesses
	References
8 Love and Marriage
	Looking at unmarried people
	Married people don't lie
	Minos and aminos: we are both married
	Minos and aminos: we are both married or both unmarried
	Married in company
	Teresa's family
	Who is Helen's husband?
	Arranged royal marriage
	Two singles at the end of the row
	Five couples
	A family tree
	Uncles and aunts
	References
9 Grid Puzzles
	A five in the middle
	Roses, shamrocks, and thistles
	Nine squares
	Latin square
	Magic Square
	Magic five-pointed star
	Fort Garrisons
	Star battle reloaded
	Fancy queens
	Playing Minesweeper
	References
10 Japanese Puzzles
	Killer Sudoku
	Futoshiki
	Kaos Sudoku
	Kakurasu
	Takuzu
	Kakuro
	Daily neighbours
	Kendoku
	Magic labyrinth
	Stars and arrows
	Tents and trees
	Sun and moon
	References
11 Russian Puzzles
	Young communist arranging flags
	Keep it even
	Magic triangle
	From 1 to 19
	A duel in arithmetic
	Twenty
	Order the numbers
	A mysterious box
	The courageous garrison
	A grouping of integers 1 to 15
	A star
	The hexagon
	Reference
12 Polyomino Puzzles
	A simple polyomino
	Rotating polyomino
	Fixed Ten-Yen
	Rotating Ten-Yen
	The twelve pentominoes
	Importing six pentominoes
	Importing other six pentominoes
	Twelve pentominoes on a chessboard
	Five tetrominoes on a strange shape
	Broken chess
	References
13 Self-reference and Other Puzzles
	Tricky messages
	Not so tricky messages
	Six tricky messages
	Which hand?
	An ornament for a window
	At the brook
	A car tour
	A diamond ring
	Drinker paradox
	Ten sentences
	Ten relaxed sentences
	Self-counting sentences
	References
Appendix A The Epigraph Puzzle