Simple problems that resist routine logic tempt one to waste time. Often, a clever idea makes a result obvious, but a formal proof takes time and space.
This note presents a new result on a well-known “tough nut.” The “nut” is the placing of dominoes on a chess board with two opposite corner squares missing. Each square has half a domino. Each domino covers two adjacent squares. I have used this problem with undergraduate computer science students. They, with a little prompting, prove that it is impossible. The author examines proof techniques used in artificial intelligence and logic programming. He proves an exponential lower bound for the size of these proofs. While reading this note, I tackled the four-by-four case by hand, using a semantic tableau, and using Prolog. The results were consistent with his lower bound.
The note presents another obvious result with a convoluted proof. The author’s bound seems obvious given the tighter bound he quotes[1]. Nevertheless, he presents a clever and intricate proof. It reduces the chess board problem to the construction of an infinite roadway of four-by-four tilings of the chess board. His proof techniques seem novel. They would benefit from a longer exposition. A long proof of a known result only deserves a short note, however.
Only proof theory professionals should study this note.