John McCarthy
Computer Science Department
Stanford University
jmc@cs.stanford.edu
http://www-formal.stanford.edu/jmc/
February 28, 1996
An 8 by 8 checkerboard with two diagonally opposite squares removed
cannot be covered by dominoes each of which covers two rectilinearly
adjacent squares. We present a set theory description of the
proposition and an informal proof that the covering is impossible.
While no present system that I know of will accept either the formal
description or the proof, I claim that both should be admitted in any
heavy duty set theory.
We have the definitions
and
If we are willing to be slightly tricky, we can write more compactly
but then the proof might not be so obvious to the program.
Next we have.
Theorem:
Proof:
We define
and finally
Q.E.D.
