Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
The Mutilated Checkerboard Back to

The Mutilated Checkerboard

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 .

The mutilated checkerboard can be stated and solved in Mizar. The formal description of the problem as presented by McCarthy is directly expressible in Mizar. However, Mizar is only a proof checker, and the solution required to write a proof about 300 lines long (as of March 1996). See a short note presenting the solution: .ps.gz , .dvi . (Available also by ftp as a TR96-09 .)

Piotr Rudnicki, email: piotr@cs.ualberta.ca