%A John McCarthy
%T A Tough Nut for Proof Procedures
%X 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,.
%D 1964
%L cogprints414

<script src="//archive-bar.soton.ac.uk/archive-bar.js"></script>