The Logic Theorist: a machine that proved theorems before AI had a name
Before a single instruction ran on a machine, Herbert Simon assembled his wife, three children, and several graduate students in January 1956, handed each of them a 3×5 index card, and asked them to follow rules. Each person was a subroutine. Together they formed a living program — a human simulation of a machine designed, in turn, to simulate human reasoning.
That machine was the Logic Theorist, and before the year was out, it had proved 38 of the first 52 theorems in Principia Mathematica.
Simon and Allen Newell had been working the idea since early 1955, joined by J. C. “Cliff” Shaw, a programmer at the RAND Corporation in Santa Monica. Newell’s insight came first: attending Oliver Selfridge’s 1954 presentation on pattern matching, he realized that a general-purpose symbol manipulator could, in principle, do what a mind did. Simon, a political scientist who had spent his career studying how organizations make decisions, supplied the theory of how humans actually solve hard problems. Shaw wrote the code.
The program ran on RAND’s JOHNNIAC — a vacuum-tube computer patterned after the von Neumann architecture — in a language the three of them invented for the purpose: IPL, the Information Processing Language, a precursor to the list-processing languages that followed. Their target was Principia Mathematica, Alfred North Whitehead and Bertrand Russell’s 1910–1913 monument that tried to rebuild all of mathematics from formal logic. The Logic Theorist worked through Chapter 2 — 52 theorems in propositional calculus — and proved 38 of them.
For Theorem 2.85, the machine went further than expected. It found a proof two steps shorter than the one Whitehead and Russell had produced by hand — and by most readings, more elegant. Simon sent the new proof to Russell. Russell, then in his mid-eighties, responded with delight.
Simon and Newell decided to submit that proof to The Journal of Symbolic Logic, listing the authors as Newell, Simon, and the Logic Theorist itself. The journal declined. A new proof of an elementary theorem was not worth their pages; the fact that the prover was a machine went apparently unremarked.
That August, at the Dartmouth Summer Research Project where John McCarthy coined the term “artificial intelligence,” the Logic Theorist should have been the star. The reception was lukewarm. The other attendees were mostly occupied with their own proposals. Newell and Simon later observed, with characteristic dryness, that the conference had been organized to pursue exactly what they had already done.
What made it matter was the method. The Logic Theorist worked by heuristic search: not exhaustive enumeration — which would have exploded exponentially — but rules of thumb for guessing which proof paths were worth pursuing. It was an attempt to replicate the educated judgment an experienced mathematician brings to a problem before committing to a line of argument. This was the first time a machine had solved a hard problem not by calculation but by something resembling taste.
Within two years, Newell and Simon had generalized the idea into the General Problem Solver. Newell eventually joined Simon at Carnegie Institute of Technology, where their AI research group became one of the most productive in the world. Simon received the Nobel Memorial Prize in Economic Sciences in 1978 — in part for formalizing the idea the Logic Theorist had first demonstrated: that human reasoning follows rules bounded enough for a machine to follow.
Formal logic had spent three thousand years as philosophy. Newell, Simon, and Shaw spent a Christmas break turning it into a program.
Sources
- Logic Theorist — Wikipedia — creation dates, the 38 theorems proved, Theorem 2.85, Russell’s reaction, the Journal of Symbolic Logic rejection.
- The First AI, Logic Theorist — Popular Science — heuristic search method, Simon’s January 1956 classroom announcement.
- Early AI Programs: The Logic Theorist (1955–1956) — ai-researchs.com — JOHNNIAC computer, IPL language.
- Logic Theorist — A History of AI — human card simulation, Newell’s 1954 epiphany.