TY  - GEN
ID  - cogprints414
UR  - http://cogprints.org/414/
A1  - McCarthy, John
TI  - A Tough Nut for Proof Procedures
Y1  - 1964/07//
N2  - 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,.
AV  - public
ER  -