Primary evidence
- A Machine-Oriented Logic Based on the Resolution PrincipleS1 · Primary research · Paper · 1965-01-01
Robinson's resolution principle establishes a machine-oriented foundation for automated deduction
The method combines substitution through unification with a single resolution inference scheme, replacing less efficient alternating procedures used in earlier machine theorem proving.
What happened?
J. A. Robinson introduced a resolution-based procedure for first-order predicate logic designed to improve the efficiency and practical applicability of machine theorem proving.
Why it matters
Resolution became one of the central algorithmic foundations of automated deduction, logic programming and many later theorem-proving systems.
Significance rationale: Robinson's resolution principle supplied a machine-oriented inference rule and unification-centered framework that became foundational to automated first-order theorem proving.
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
- Computation only
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- New algorithm
- Interface
- Formal, Symbolic
- AI contribution
- The event concerns an algorithmic inference method designed for machine reasoning rather than an AI system producing a new mathematical theorem.
- Human contribution
- J. A. Robinson developed and analyzed the resolution principle and its machine-oriented logical formulation.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- —
- Organizations
- argonne-national-laboratory
- Problems
- first-order-theorem-proving
- Methods
- resolution, unification, automated-deduction
Sources & artifacts
- A Machine-Oriented Logic Based on the Resolution PrincipleS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 1965-01-01 · Paper released · E2 · Research record
The JACM research record establishes the resolution principle and its machine-theorem-proving motivation.
Corrections
No corrections recorded.