Logic Theorist: First AI Program
Allen Newell and Herbert Simon create Logic Theorist, the first AI program capable of proving mathematical theorems.
Overview
In 1956, Allen Newell and Herbert Simon developed Logic Theorist at RAND Corporation, considered the first artificial intelligence program. Logic Theorist could automatically prove theorems from Whitehead and Russell's "Principia Mathematica", sometimes finding proofs more elegant than the originals. The program used heuristic search to explore possible proof paths, simulating the reasoning process of human mathematicians. Logic Theorist was demonstrated at the Dartmouth Conference, along with the "Information Processing Language" (IPL), one of the earliest list processing languages.
Study Notes
Background, mechanics, impact, and key takeaways in one read
Background & Context
Between 1955 and 1956, Allen Newell, Herbert Simon, and J.C. Shaw built the Logic Theorist at the RAND Corporation; it is widely called the first artificial-intelligence program. While others debated whether machines could "think," the trio took a different tack: rather than build a general mind, build a program that mimicked a human mathematician proving logical theorems by heuristic search. They picked Whitehead and Russell's Principia Mathematica from a shelf as a target—not to advance logic, but because it was complex, non-numerical, and perfect for showing a machine could discover proofs in a symbolic domain using human-like heuristics. They first demonstrated it at the 1956 Dartmouth workshop, marking AI's birth as an experimental field.
Key Points
- 1Developed by Newell, Simon, and Shaw in 1955–56 at RAND, the program was written in the IPL language.
- 2Its goal was to prove theorems automatically within the propositional calculus of Whitehead and Russell's Principia Mathematica.
- 3It proved 38 of the first 52 theorems in Chapter 2, and some proofs were more elegant than the original.
- 4It used heuristic search by backward reasoning, working from the target theorem back toward smaller subgoals.
- 5Demonstrated at the 1956 Dartmouth workshop, it was hailed by Minsky as the first working AI program.
- 6A paper on it was rejected by the Journal of Symbolic Logic for merely "reproving known theorems."
How It Works
The Logic Theorist treated theorem-proving as searching a logical path from axioms to a goal within a symbol space. Rather than enumerate, it used heuristic search: starting from the target theorem, it reasoned backward to find subgoals and applicable rules, recursively breaking a big problem into smaller, immediately decidable ones until every branch landed on a known axiom. In other words, it mimicked a mathematician who first clarifies what must be shown, then works backward to the lemmas needed—not blind trial. Running on the IBM 704, its core was symbolic-list manipulation and rule deduction; it was written in IPL, the first list-based programming language designed for AI, which directly inspired LISP.
Impact & Legacy
The Logic Theorist established the symbolic-AI paradigm: intelligence equals search and transformation over symbol structures. It directly spawned the General Problem Solver and influenced LISP's list processing. Within automated theorem proving its impact was limited—Hao Wang proved all of Principia's first-order theorems in nine minutes in 1958, showing the method was not the most efficient. Its true legacy was proving that heuristic-guided search works, laying the foundation for expert systems and cognitive science, and launching computational models of how humans solve problems.
Key Takeaways
- Intelligence need not start with "understanding"; systematically searching and rewriting symbols already shows reasoning.
- Abstracting a general mechanism from one concrete task is a common AI engineering path.
- The rejection for "reproving known theorems" reminds us that methodological novelty can outweigh result novelty.
Glossary
A search strategy that uses rules of thumb to explore promising paths first, avoiding exhaustive enumeration of the space.
The first list-processing language designed for AI; the Logic Theorist was written in it, and it preceded LISP.
Starting from the goal to be proved and working backward to subgoals and rules until known axioms are reached.