Research · August 1956

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

Related events

Related Dartmouth Summer Research Project
The program was shown to the Dartmouth workshop participants that summer.
Builds on Newell's chess machine
Goal-directed search carried over from the chess task to theorem proving.
The logic theory machine: A complex information processing system

Records that link to this one

Builds on General Problem Solver
GPS separates the search strategy, worked out in Logic Theorist, from the subject domain.
Report on a General Problem-Solving Program
Related Computers and Thought
The collection reprinted the key Newell, Shaw and Simon papers.
Contrasts Hao Wang: Principia in minutes
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
Related Automath: a language in which a machine checks mathematics
Logic Theorist searched for proofs itself; Automath sets a different task: the machine checks every line of a proof a person wrote.