Logic Theorist

The program by Newell, Shaw and Simon proved theorems from Principia Mathematica by searching plausible derivations rather than all of them.

Why it matters

The first program to do work considered exclusively human, and to do it by heuristic search rather than enumeration.

Logic Theorist proved 38 of the first 52 theorems in chapter two of Principia Mathematica, and found a shorter proof of theorem 2.85 than Whitehead and Russell's. The Journal of Symbolic Logic rejected a paper that listed the program as a co-author. To build it, Newell and Shaw created the IPL list-processing language.

Event record

Event date

August 1956 · Approximate date

Timeline date

Event date

Verification

Sources gathered automatically · September 17, 2026

Lines

ID

evt-0082

The first machine proofs were produced in August 1956 on the JOHNNIAC; some results, including the shorter proof of theorem 2.85, come from runs in late 1956 and early 1957. The month is approximate.

Sources

primary The logic theory machine: A complex information processing system
IRE Transactions on Information Theory · Published September 1956
secondary The Quest for Artificial Intelligence (Nilsson), section 5.1 The Logic Theorist and Heuristic Search
Nils J. Nilsson, Cambridge University Press (author's Stanford copy) · Published 2010
archive The Logic Theory Machine - A Complex Information Processing System (Feigenbaum papers, Stanford Special Collections)
Stanford University Libraries · Published July 12, 1956

Related events

Earlier

Builds on Newell's chess machine 1955
Goal-directed search carried over from the chess task to theorem proving.
- The logic theory machine: A complex information processing system · IRE Transactions on Information Theory

Same period

Related Dartmouth Summer Research Project 1956
The program was shown to the Dartmouth workshop participants that summer.

Later

Builds on A chess program built from goals, not numbers 1958links to this record
The paper ties chess directly to the programs that find proofs of theorems in symbolic logic: both tasks are reasoning with heuristics in a space that grows exponentially.
- A. Newell, J. C. Shaw, H. A. Simon, «Chess-Playing Programs and the Problem of Complexity», RAND Corporation paper P-1319, 4 September 1958 («To be published in the IBM Journal of Research and Development») · RAND Corporation (copy: bitsavers.org through the Internet Archive)
Builds on General Problem Solver 1959links to this record
GPS separates the search strategy, worked out in Logic Theorist, from the subject domain.
- Report on a General Problem-Solving Program · RAND Corporation
Contrasts Hao Wang: Principia in minutes 1960links to this record
Wang compares his programs directly with Logic Theorist: the 52 theorems Newell, Shaw and Simon chose were proved in under 5 minutes, and he sets complete algorithms against their heuristics.
- Toward Mechanical Mathematics (Hao Wang), IBM Journal of Research and Development 4(1), 2-22 · IBM (scan on bitsavers.org)
Related Computers and Thought 1963links to this record
The collection reprinted the key Newell, Shaw and Simon papers.
Related Automath: a language in which a machine checks mathematics 1968links to this record
Logic Theorist searched for proofs itself; Automath sets a different task: the machine checks every line of a proof a person wrote.