A Tough Nut for Proof Procedures,

Abstract

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. It is conjectured that this problem will be very difficult for programmed proof procedures. (Modified author abstract)

Document Details

Document Type
Technical Report
Publication Date
Jul 17, 1964
Accession Number
AD0785037

Entities

People

  • John McCarthy

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Applied Computer Science
  • Artificial Intelligence
  • Calculus

Readers

  • Graph Algorithms and Convex Optimization.
  • Systems Analysis and Design