Technical reports

A simple formalization and proof for the mutilated chess board

Lawrence C. Paulson

April 1996, 11 pages

DOI: 10.48456/tr-394

Abstract

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. is applicable in a variety of domains.

Full text

PDF (0.1 MB)
PS (0.0 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-394,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{A simple formalization and proof for the mutilated chess
         	   board}},
  year = 	 1996,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-394.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-394},
  number = 	 {UCAM-CL-TR-394}
}