This is a decommissioned version of ERA which is running to enable completion of migration processes. All new collections and items and all edits to existing items should go to our new ERA instance at https://ualberta.scholaris.ca - Please contact us at erahelp@ualberta.ca for assistance!
- 379 views
- 148 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