A Machine-Oriented Logic Based on the Resolution Principle
A complete source map of Robinson's 1965 resolution paper, including clause semantics, ground and first-order refutation completeness, standardization apart, most-general unification, the occurs check, generalized resolution, and nonterminating proof search.
Robinson's paper presents resolution as a sound, effective, machine-oriented inference principle and develops the substitution and unification machinery needed to lift ground resolution to first-order clauses. It is primary authority for the historical calculus and its completeness proof, while modern teaching often decomposes its generalized multi-literal rule into binary resolution plus a separate factoring rule.
The archived object is a 19-page scan of Journal of the ACM 12(1), printed pages 23–41. All pages were read and visually inspected at 180 dpi. Its embedded OCR is noisy, so empty-clause symbols, set relations, algorithms, and aligned derivations were read from the raster surface. The PDF has SHA-256 757c6bcef2e07fdae1e604cea0556413b82ad46f3f26d62dbc20f30675b9886b.
Source map #
| Printed pages | Material | GTK use |
|---|---|---|
| 23–24 | Motivation and formal preliminaries | Historical orientation and machine-oriented goal |
| 25–26 | Literals, clauses, empty clause, empty clause set, Herbrand semantics, ground resolution | Clause semantics and ground soundness |
| 27–30 | Saturation, Ground Resolution Theorem, Basic Lemma, Resolution Theorem | Refutation completeness and finite-input scope |
| 30–34 | Substitutions, standardization apart, disagreement sets, unification algorithm, MGU | First-order inference mechanism and occurs check |
| 33–36 | Generalized resolvents, refutations, worked derivations | Historical calculus and completeness |
| 37–40 | Infinite closure, purity, subsumption, replacement | Search nontermination and redundancy control |
| 41 | Bibliography and manuscript history | Identity and source-defect cross-check |
Claims retained with scope #
- A clause is a finite, possibly empty set of literals. A clause set containing the empty clause is unsatisfiable, whereas the empty set of clauses is satisfiable.
- Ground resolution preserves every model of its parents, and exhaustive ground closure is refutation-complete for finite ground clause sets.
- Separate parent clauses must be standardized apart before unification.
- Robinson's unification algorithm rejects a variable replacement in which that variable occurs and returns a most-general unifier through which every other unifier factors.
- The generalized resolvent may select several literals from each parent and unify all corresponding atoms. This absorbs multi-literal merging into resolution; the paper does not define a separately named factoring rule.
- A finite first-order clause set is unsatisfiable exactly when a finite generalized-resolution refutation exists.
- First-order closure can be infinite. Completeness guarantees that exhaustive enumeration eventually finds a refutation for unsatisfiable finite input, not that every search strategy terminates.
Source defects and boundaries #
- Printed page 28 cites Davis–Putnam as reference
[4], while the bibliography identifies that work as[2]; the error is bibliographic. - The Subsumption Algorithm on printed page 39 directs step 1 to step 3, skipping initialization in step 2. The surrounding proof makes step 2 the coherent target.
- The paper does not supply GTK's modern Tseitin transformation, full clausification/Skolemization contract, or explicit fairness terminology. Those are independent modern parts of the chapter.
Visual audit #
The two information-bearing layouts are an aligned clause derivation on printed page 36 and an underlined deletion sequence on printed page 40. Both were inspected, but neither is retained: they serve historical examples rather than the chapter's core mechanism, and independently typeset modern examples are clearer and more accessible.