title: A Tough Nut for Proof Procedures
creator: McCarthy, John
subject: Artificial Intelligence
description: 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,.
date: 1964-07
type: Preprint
type: NonPeerReviewed
format: application/postscript
identifier: http://cogprints.org/414/2/toughnut.ps
identifier:   McCarthy, John  (1964) A Tough Nut for Proof Procedures.  [Preprint]     
relation: http://cogprints.org/414/