The resolution principle

Robinson reduced proof in first-order logic to a single inference rule fit for a machine.

Why it matters

Automatic theorem proving became feasible, and later turned into logic programming.

The key part is the unification algorithm, which finds the most general substitution for two expressions. The method works by refutation: the negation of the goal is added to the set of statements and a contradiction is sought. Prolog in 1972 is built on a restricted form of the same mechanism.

Event record

Event date

January 1965

Timeline date

Event date

Verification

Sources gathered automatically · September 17, 2026

Lines

ID

evt-0103

The January 1965 issue of the Journal of the ACM.

John Alan Robinson

Sources

primary A Machine-Oriented Logic Based on the Resolution Principle
Journal of the ACM · Published January 1965
secondary The Early Years of Logic Programming, R. Kowalski
Communications of the ACM 31(1) (copy on the author's page at Imperial College) · Published 1988

Related events

Earlier

Related Programs with Common Sense 1958
Resolution supplied the inference mechanism the advice taker scheme lacked.

Later

Builds on Shakey 1969links to this record
Action planning was built on resolution theorem proving.
- A Mobile Automaton: An Application of Artificial Intelligence Techniques · IJCAI-69
Contrasts STRIPS 1971links to this record
Instead of full logical inference, an action is described by add and delete lists.
- STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving · Artificial Intelligence
Related Cook's theorem 1971links to this record
The paper states its result about the complexity of theorem-proving procedures.