This decommissioned ERA site remains active temporarily to support our final migration steps to https://ualberta.scholaris.ca, ERA's new home. All new collections and items, including Spring 2025 theses, are at that site. For assistance, please contact erahelp@ualberta.ca.
- 401 views
- 153 downloads
The Mutilated Checkerboard Problem in the Lightweight Set Theory of Mizar
-
- Author(s) / Creator(s)
-
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
-
- Type of Item
- Report
-
- License
- Attribution 3.0 International