AI/ML Wiki

robinson-1965-a-machine-oriented-logic-based-on

4 min read

A Machine-Oriented Logic Based on the Resolution Principle

Authors: J. A. Robinson
Year: 1965 | Journal of the ACM
Source: robinson-1965-a-machine-oriented-logic-based-on

What it is

Robinson’s 1965 paper gave symbolic AI its inference engine. The resolution principle is a single inference rule that is both sound and complete for first-order logic. Combined with the unification algorithm, it makes mechanical theorem proving practical — replacing the exponentially explosive Herbrand-based methods that preceded it. Prolog, logic programming, and automated reasoning all descend directly from this paper.

The problem it solved

Automated theorem proving before 1965 used Herbrand’s theorem: to prove a sentence unsatisfiable, generate substitutions and check truth-functionally.

The process:

  1. Generate substitutions of terms for variables
  2. Check if the resulting ground clauses are truth-functionally contradictory
  3. If not, generate more complex substitutions and repeat

The problem: steps 1 and 2 alternate in a cycle, and the substitution space explodes combinatorially. For all but trivial theorems, it was computationally infeasible.

Robinson’s insight: substitution and truth-functional analysis can be merged into one step.

Unification

Two atoms unify if there exists a substitution that makes them identical:

P(x, f(y))  and  P(a, f(b))
             ↓
Most General Unifier (MGU): {x=a, y=b}

The MGU is the least-committal unifier — it makes no assumptions beyond what’s needed.

Unification is computed in polynomial time. It’s the core of every logic programming language.

The Resolution Rule

To apply resolution:

  1. Take two clauses containing complementary literals: C₁ with literal L, and C₂ with literal ¬L’ where L and L’ unify via MGU θ
  2. Remove the complementary literals and merge the remaining literals (under substitution θ)
C₁ = P(x) ∨ Q(x)
C₂ = ¬P(a) ∨ R(a)
MGU: {x = a}
Resolvent: Q(a) ∨ R(a)

Each resolution step simultaneously instantiates variables AND eliminates a pair of complementary literals. This is what makes it so much more efficient than the two-stage Herbrand approach.

Completeness (refutation)

Resolution is refutation complete: if a set of clauses is unsatisfiable, applying resolution repeatedly will eventually derive the empty clause □ (a contradiction).

To prove theorem T from axioms A:

1. Assume ¬T
2. Add ¬T to A → new clause set S
3. Apply resolution repeatedly
4. If □ is derived → S is unsatisfiable → A ⊨ T

This is how all logic programming and automated theorem proving works.

Why it matters for symbolic AI

McCarthy’s Advice Taker (1958) needed a reasoning engine — a way to automatically derive consequences from a knowledge base. Resolution is that engine.

Knowledge base:
  (1) human(Socrates)
  (2) human(x) → mortal(x)     ≡ ¬human(x) ∨ mortal(x)
  
Goal: prove mortal(Socrates)
  → Assume ¬mortal(Socrates)
  → Resolve (2) with ¬mortal(Socrates): ¬human(Socrates)
  → Resolve with (1): □ (contradiction)
  → Therefore: mortal(Socrates) ✓

This mechanical procedure works for arbitrarily complex knowledge bases. Resolution is the difference between “we could represent knowledge in logic” and “we can actually reason with it.”

Direct descendants

SystemYearConnection
PLANNER1969Procedural embedding of resolution
Prolog1972SL-resolution + depth-first search
Otter1984High-performance resolution theorem prover
Vampire1993Industrial-strength automated reasoning
Modern SAT solvers—Propositional resolution with clause learning

Prolog in particular shows the reach: resolution + unification + depth-first search = a complete programming language based on logic. Every Prolog clause is a Horn clause; every Prolog query is a resolution refutation.

Limits

Resolution is complete but not decidable for first-order logic: for satisfiable clause sets, resolution may run forever without deriving □. The search problem — which resolvents to compute in what order — remains hard. Robinson acknowledged this and proposed “search principles” to guide the process; finding better strategies drove theorem-proving research for decades.

See also

Graph View

Backlinks