next up previous
Next: References


John McCarthy
Computer Science Department
Stanford University
Stanford, CA 94305

JanFebMarAprMayJun JulAugSepOctNovDec , :< 10 0


It is well known to be impossible to tile with dominoes a checkerboard with two opposite corners deleted. This fact is readily stated in the first order predicate calculus, but the usual proof which involves a parity and counting argument does not readily translate into predicate calculus. We conjecture that this problem will be very difficult for programmed proof procedures.

The research reported here was supported in part by the Advanced Research Project Agency of the Office of the Secretary of Defense (SD-183). gif

It is impossible to cover the mutilated checkerboard shown in the figure with dominoes like the one in the figure. Namely, a domino covers a square of each color, but there are 30 black squares and 32 white squares to be covered. This old impossibility statement is readily formulated as a sentence of the predicate calculus, but I don't see how the parity and counting argument can be translated into a guide to the method of semantic tableaus tex2html_wrap_inline55 , into a resolvent argument tex2html_wrap_inline57 , or into a standard proof. Therefore, I offer the problem of proving the following sentences inconsistent as a challenge to the programmers of proof procedures and to the optimists who believe that by formulating number theory in predicate calculus and by devising efficient general proof procedures for predicate calculus, significant mathematical theorems can be proved.

We number the rows and columns from 1 to 8 and we introduce predicates S(x,y), L(x,y), E(x,y), tex2html_wrap_inline59 , tex2html_wrap_inline61 , tex2html_wrap_inline63 , tex2html_wrap_inline65 , and tex2html_wrap_inline67 with the following intended interpretations:

S(x,y) means y = x + 1

L(x,y) means x < y

E(x,y) means x = y

tex2html_wrap_inline59 means the square (x,y) and the square (x+1,y) are covered by a domino.

tex2html_wrap_inline61 means the square (x,y) and the square (x,y+1) are covered by a domino.

tex2html_wrap_inline63 means the square (x,y) and the square (x-1,y) are covered by a domino.

tex2html_wrap_inline65 means the square (x,y) and the square (x,y-1) are covered by a domino.

tex2html_wrap_inline67 means the square (x,y) is not covered.

We shall axiomatize only as much of the properties of the numbers from 1 to 8 as we shall need.

  1. S(1,2) tex2html_wrap_inline81 S(2,3) tex2html_wrap_inline81 S(3,4) tex2html_wrap_inline81 S(4,5) tex2html_wrap_inline81 S(5,6) tex2html_wrap_inline81 S(6,7) tex2html_wrap_inline81 S(7,8)
  2. S(x,y) tex2html_wrap_inline93 L(x,y)
  3. L(x,y) tex2html_wrap_inline81 Lyz tex2html_wrap_inline93 Lxz tex2html_wrap_inline81 tex2html_wrap_inline101 S(x,z)
  4. L(x,y) tex2html_wrap_inline93 tex2html_wrap_inline101 E(x,y)
  5. E(x,x)

    These axioms insure that all eight numbers are different and determine the values of S(x,y), L(x,y), and E(x,y) for x, y = 1, tex2html_wrap_inline107 , 8.

  6. tex2html_wrap_inline109
  7. tex2html_wrap_inline111
  8. tex2html_wrap_inline113
  9. tex2html_wrap_inline115
  10. tex2html_wrap_inline117

    These axioms insure that every square (x,y) satisfies exactly one tex2html_wrap_inline119

  11. tex2html_wrap_inline121
  12. tex2html_wrap_inline123 These axioms insure that the uncovered squares are precisely (1,1) and (8,8).
  13. tex2html_wrap_inline125
  14. tex2html_wrap_inline127 These axioms state the conditions that a pair of adjacent squares be covered by a domino.
  15. tex2html_wrap_inline129

These axioms state that the dominoes don't stick out over the edge of the board.

Suppose we had a model of these 15 sentences (in Robinson's clausal formalism, there would be 31 clauses). There would have to be eight individuals tex2html_wrap_inline131 satisfying the relations asserted for tex2html_wrap_inline133 in the axioms. They would have to be distinct since axioms 1,2, and 3 allow us to prove L(x,y) whenever this is so and axioms 4 and 5 then allow us to show that L(x,y) holds only for distinct x and y.

We then label the squares of a checkboard and place a domino on each square (x,y) that satisfies tex2html_wrap_inline59 or tex2html_wrap_inline61 sticking to the right or up as the case may be. Axioms 13 and 14 insure that the dominoes don't overlap, axioms 6-12 insure that all squares but the corner squares are covered and axiom 15 insures that no dominoes stick out over the edge.

Since there is no such covering the sentences have no model and are inconsistent.

In a formalism that allows functions and equality we have a briefer inconsistent set of sentences involving

s(x)the successor of x

g(x,y) has value of 1 to 5 according to whether tex2html_wrap_inline59 or tex2html_wrap_inline107 or tex2html_wrap_inline67

The sentences are

  1. s(s(s(s(s(s(s(s(8)))))))) = 8
  2. tex2html_wrap_inline155

    The sentences insure the existence of 8 distinct individuals using a cyclic successor function.

  3. g(x,y) = 5 tex2html_wrap_inline157 x = 8 tex2html_wrap_inline81 y = 8 tex2html_wrap_inline161 x = 1 tex2html_wrap_inline81 y = 1

    Insures that exactly the corner squares (1,1) and (8,8) are uncovered.

  4. g(x,y) = 1 tex2html_wrap_inline157 g(s(x),y) = 3
  5. g(x,y) = 2 tex2html_wrap_inline157 g(x,s(y)) = 4

    Each domino covers two adjacent squares

  6. tex2html_wrap_inline169

    Dominoes don't stick out

  7. 1 = s(8) tex2html_wrap_inline81 2 = s(1) tex2html_wrap_inline81 3 = s(2) tex2html_wrap_inline81 4 = s(3) tex2html_wrap_inline81 5 = s(4)
  8. g(x,y) = 1 tex2html_wrap_inline161 g(x,y) = 2 tex2html_wrap_inline161 g(x,y) = 3 tex2html_wrap_inline161 g(x,y) = 4 tex2html_wrap_inline161 g(x,y) = 5

Identifies the numbers used and ties down the values of g.

next up previous
Next: References

John McCarthy
Sat Jan 2 17:30:32 PST 1999