The Logic Theorist: first automatic theorem-proving program, developed by Newell, Shaw, and Simon
In late 1955, Allen Newell, J. Clifford Shaw, and Herbert A. Simon at RAND Corporation and Carnegie Institute of Technology completed the Logic Theorist, a computer program that proved mathematical theorems from Whitehead and Russell's Principia Mathematica by heuristic search, establishing that symbolic reasoning could be mechanised.
Background
By the early 1950s, computers were understood as machines for calculation. They could add, multiply, sort and tabulate at speeds no person could match. What they could not do, or so most researchers assumed, was reason. Reasoning meant working with symbols and rules, not numbers, and no one had shown a machine could manage that.
The mathematics of formal logic had given logicians a precise language for symbolic argument since the late nineteenth century. Bertrand Russell and Alfred North Whitehead laid it out systematically in Principia Mathematica, published between 1910 and 1913, where they derived hundreds of theorems in propositional and predicate logic from a small set of axioms. The proofs were mechanical in a certain sense: each step followed from the last by a defined rule. But finding which rules to apply, and in which order, was another matter. The number of possible sequences grew faster than any exhaustive search could handle.
The standard response to a hard search problem, at the time, was to look everywhere. Try every combination and stop when you find an answer. That works well enough for small problems. For something like theorem-proving, where the space of possible proof steps expands at each branch, it was hopeless.
What happened
Allen Newell, a researcher at RAND Corporation in Santa Monica, J. Clifford Shaw, a programmer also at RAND, and Herbert A. Simon, an economist and cognitive psychologist at Carnegie Institute of Technology in Pittsburgh, set out to do something different. Rather than search exhaustively, they built a program that searched selectively. It used heuristics, which are rules of thumb that make some paths look more promising than others and let the program skip large parts of the search space without checking them. Their program was called the Logic Theorist.
The Logic Theorist worked with the symbolic logic of Principia Mathematica directly. Given a theorem to prove, it would try to work backwards from the target, looking for known results that could bridge the gap. It held expressions not as numbers but as structured symbolic objects, a design that required Shaw to build new programming tools capable of handling that kind of data, since nothing suitable yet existed.
By December 1955, the program was running well enough for Simon to demonstrate it to his class at Carnegie. In tests against the theorems in Principia Mathematica, it succeeded in proving 38 of the first 52 propositions in Chapter 2. One of its proofs was, by some measures, more elegant than the one Russell and Whitehead had published. Simon, Newell and Shaw submitted the result to the Journal of Symbolic Logic, listing the Logic Theorist as co-author. The journal declined to accept it on those terms. The work was published in full in 1957 in the proceedings of the Western Joint Computer Conference, under the title “Empirical Explorations with the Logic Theory Machine.”
The program reached a wider audience when Newell and Simon presented it at the Dartmouth Summer Research Project in the summer of 1956, a gathering that brought together most of the researchers then working on machine intelligence. The Logic Theorist did not prove every theorem it attempted, and it was not designed to generalise beyond the specific domain of propositional logic. But it showed, concretely and for the first time, that a machine could search a symbolic space by judgement rather than brute force.
Why it mattered
The Logic Theorist demonstrated for the first time that a digital computer could perform non-numerical symbolic reasoning, directly challenging the assumption that machines were limited to arithmetic. It introduced heuristic search (guided, selective exploration of a problem space) as a core method that would underpin AI research for decades. Its public presentation at the 1956 Dartmouth Conference helped constitute artificial intelligence as a recognised field of scientific inquiry.
People
Allen Newell, J Clifford Shaw, Herbert A Simon
Organisations
RAND Corporation, Carnegie Institute of Technology
Sources
- Empirical explorations with the logic theory machine: a case study in heuristics.ACM, Proceedings of the Western Joint Computer Conference, 1957.Primary source
- Newell and Simon's Logic Theorist: Historical Background and Impact on Cognitive Science.Proceedings of the Human Factors and Ergonomics Society Annual Meeting (SAGE Journals).Secondary
- Cognitive architectures and rational analysis: Comment.Psychological Review (APA).Secondary
Cite this page
AI Achievements. (1955). The Logic Theorist: first automatic theorem-proving program, developed by Newell, Shaw, and Simon. Retrieved 2026-08-22, from https://achievements.ai/milestone/the-logic-theorist-first-ai-program-ever
@misc{achievements_the_logic_theorist_first_ai_program_ever,
title = {The Logic Theorist: first automatic theorem-proving program, developed by Newell, Shaw, and Simon},
author = {{AI Achievements}},
year = {1955},
url = {https://achievements.ai/milestone/the-logic-theorist-first-ai-program-ever}
}