Communities and Collections
Usage
- 280 views
- 111 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