Primary evidence
- The Logic Theory Machine — A Complex Information Processing SystemS1 · Primary research · Paper · 1956-09-10
Logic Theorist demonstrates machine-generated proofs in symbolic logic
The system encoded logical expressions and searched a space of permissible transformations, prioritizing promising branches with heuristics rather than exhaustive enumeration.
What happened?
Newell, Shaw and Simon presented the Logic Theory Machine in 1956 as a program that searched for proofs of propositions from Principia Mathematica using symbolic representations and heuristics.
Why it matters
It established mathematical theorem proving as one of the earliest concrete demonstrations of symbolic AI and set a durable precedent for treating proof search as intelligent problem solving.
Significance rationale: Logic Theorist is a foundational early example of artificial intelligence applied directly to mathematical proof, using heuristic search to construct proofs of symbolic-logic propositions.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Autonomous primary role
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Rediscovery
- Interface
- Formal, Symbolic
- AI contribution
- The program selected transformations and assembled proofs through automated heuristic search.
- Human contribution
- Researchers designed the representation, heuristics, search procedure and evaluation corpus.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- logic-theorist
- Organizations
- rand-corporation, carnegie-tech
- Problems
- symbolic-logic-theorem-proving
- Methods
- heuristic-search, symbolic-reasoning, proof-search
Sources & artifacts
- The Logic Theory Machine — A Complex Information Processing SystemS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 1956-09-10 · Paper released · E2 · Research record
RAND P-868 records the 1956 Logic Theory Machine and its symposium presentation.
Corrections
No corrections recorded.