## A Simple Formalization and Proof for the Mutilated Chess BoardAbstract: "The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are straightforward except for some lemmas concerning finite cardinalities. This exercise is an object lesson in choosing a good formalization." |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction Ml Is 2 Mathematical development iJ irf | 2 |

The mechanical proof | 4 |

Related work | 6 |

1 other sections not shown

### Common terms and phrases

addls tiling.intrs addss addsimps evnodd.def addss HOL.ss addsimps ALLGOALS asm.simp.tac Isimpset asm.full.simp.tac asm.simp.tac Isimpset addsimps assume.tac below.def below.less.iff RS iffDl below(n below(Suc car s2 card(evnodd Cartesian product d:domino diagonally opposite squares disjoint tilings domino.elim domino.finite domino.singleton RS exE dominoes.tile.matrix dominoes.tile.row eq.cs eresolve.tac tiling.induct etac tiling.induct evnodd.empty evnodd.insert evnodd.subset RS finite.subset fast.tac prod.cs addls fast.tac set.cs finite.emptyl finitely many squares formalization goal thy goalw thy evnodd.def HOL.ss addsimps Un.assoc inductive definitions insert i,j intrs Isabelle Isabelle/HOL Isimpset addsimps below.Suc less.irrefl mod.less mod2.cases RS disjE mutilated board mutilated chess board nat.ind.tac nat.rec nat*nat)set natural numbers nl+nl odd squares prod.cs addls equalityl prove res.inst.tac kl rtac set evnodd set theory set.cs addls tiling.intrs setloop split.tac expand.if Sigma.Sucl simp.tac Isimpset addsimps squares as odd step.tac subgoal.tac subset.empty.iff RS sym Suc(m+m Suc(n+n Suc(nl+nl t:tiling tiled using dominoes tiled with dominoes tiling domino tiling.domino.0.l tiling.domino.finite tiling.intrs addss HOL.ss tiling.Unl tiling(A Type theory