Articles

A Tough Nut for Proof Procedures

This Stanford AI Memo of 1964 illustrated the fact that a theorem may not be easy to prove if the proof involves an idea not expressible in the language in which the theorem is stated.

It is well known to be impossible to tile with dominoes a checker-board 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).

Download the article in PDF.