Carnegie Institute of Technology (CMU AI Lab)

Contribution to AI

The first convincing demonstration that a machine could do something people were willing to call reasoning was a theorem prover. Logic Theorist, running on RAND's JOHNNIAC and shown at the Dartmouth meeting in the summer of 1956, proved thirty-eight of the first fifty-two theorems in chapter two of Principia Mathematica, and found one proof shorter than Whitehead and Russell's own. Making it run required inventing the substrate: Newell, Simon and Cliff Shaw built the Information Processing Languages around linked lists, recursion and dynamically allocated symbol structures, and every symbolic programme of the next thirty years, LISP included, worked with those materials. The Pittsburgh group's second move was methodological and arguably the more durable. Recording people thinking aloud as they worked through puzzles and cryptarithmetic, then writing programmes whose intermediate steps could be lined up against the transcripts, gave psychology and programming a shared test — the trace either matched or it did not. Human Problem Solving set this out in 1972 together with the framing of a task as search through a problem space and the means-ends heuristic that planning research still assumes. Underneath sat the claim stated flatly in their 1975 Turing lecture, that a physical symbol system has the necessary and sufficient means for general intelligent action: the sharpest hypothesis anyone offered, and the one the field has spent decades testing against it.

Drafted with AI and edited by hand (claude-opus-5, reviewed 2026-08).