Modelling Puzzles in First Order Logic

Description

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