The Mutilated Checkerboard Problem in the Lightweight Set Theory of Mizar

• Author(s) / Creator(s)

  • Rudnicki, Piotr

• Technical report TR96-09. An 8 by 8 checkerboard with two diagonally opposite squares removed cannot be covered by 2 by 1 dominoes. John McCarthy postulates that a mechanized system of heavy duty set theory should accept his formal description of the proposition and his proof that the covering is impossible, as presented at the QED meeting in Warsaw in 1995. This note is a report on solving the mutilated checkerboard problem in the Mizar proof checking environment. | TRID-ID TR96-09

• Date created

  1996

• Subjects / Keywords

  • Mizar proof checking environment
  • Mutilated checkerboard problem

• Type of Item

  Report

• DOI

  https://doi.org/10.7939/R3QV3C738

• License

  Attribution 3.0 International