McCarthy, John

A Tough Nut for Theorem Provers


It is impossible to cover the mutilated checkerboard shown in the figure with dominoes like the one in the figure. Namely, a domino covers a square of each color, but there are 30 black squares and 32 white squares to be covered. Therefore, I offer the problem of proving the following sentences inconsistent as a challenge to the programmers of proof procedures and to the optimists who believe that by formulating number theory in predicate calculus and by devising efficient general proof procedures for predicate calculus, significant mathematical theorems can be proved. They would have to be distinct since axioms 1,2, and 3 allow us to prove L(x, y) whenever this is so and axioms 4 and 5 then allow us to show that L(x, y) holds only for distinct x and y. Axioms 13 and 14 insure that the dominoes don't overlap, axioms 6-12 insure that all squares but the corner squares are covered and axiom 15 insures that no dominoes stick out over the edge.

Situations, Actions and Causal Laws


"A formal theory is given concerning situations, causality and the possibility and effects of actions is given. The theory is intended to be used by the Advice Taker, a computer program that is to decide what to do by reasoning. Some simple examples are given of descriptions of situations and deductions that certain goals can be achieved."Reprinted in M. Minsky (ed.), Semantic Information Processing, Cambridge, MA: MIT Press, 1968. Related topics are explored in J. McCarthy and Patrick Hayes, Some Philosophical Ideas From the Standpoint of Artificial Intelligence," MI-4, 1969.Stanford Artificial Intelligence Project Memo No 2, July 1963