Resolution and Prolog

In 1965, the logician John Alan Robinson discovered something remarkable: you can compress all of logic into a single inference rule. Given two clauses that each contain a complementary literal — one asserts $P$, the other denies $P$ — you may combine them into one clause with $P$ cancelled out. He called it resolution.

That one rule, applied repeatedly, is enough to decide whether any set of first-order logical clauses has a contradiction hidden in it. Proving a goal then becomes proof by refutation: add the negation of what you want to prove to your axioms, run resolution, and if you derive an empty clause (a contradiction), the original goal must be true.

A decade later, Alain Colmerauer and Robert Kowalski turned this into a programming language: Prolog. You write facts and rules, ask a query, and the engine systematically applies resolution — combined with unification to match variable patterns — until it finds a proof or exhausts all paths. Every Prolog execution is, at its core, a resolution proof search.

The demo below contains a small family knowledge base. Facts like parent(tom, bob) state that Tom is a parent of Bob. A rule like ancestor(X, Y) :- parent(X, Y) says X is an ancestor of Y if X is a parent of Y. Click Run query to watch the resolution steps.

<p class="hint">{{hint}}</p>
<div class="kb-area">
  <div class="kb-label">{{kb_label}}</div>
  <div id="kb" class="kb"></div>
</div>
<div class="query-row">
  <label class="kb-label" for="query">{{query_label}}</label>
  <div class="query-presets">
    <button class="preset" data-q="ancestor(tom, ann)">ancestor(tom, ann)?</button>
    <button class="preset" data-q="ancestor(bob, pat)">ancestor(bob, pat)?</button>
    <button class="preset" data-q="ancestor(tom, liz)">ancestor(tom, liz)?</button>
    <button class="preset" data-q="ancestor(ann, tom)">ancestor(ann, tom)?</button>
  </div>
  <input id="query" type="text" value="ancestor(tom, ann)" spellcheck="false" />
  <button id="run" type="button">{{run_btn}}</button>
</div>
<div id="trace" class="trace"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.5; }
.kb-label { font-size: .78rem; font-weight: 700; text-transform: uppercase;
            letter-spacing: .06em; color: #5a6a7a; margin-bottom: .3rem; }
.kb-area { background: #f4f6f8; border: 1px solid #dde3ea; border-radius: 8px;
           padding: .6rem .8rem; margin-bottom: .6rem; }
.kb { font-family: ui-monospace, monospace; font-size: .85rem; line-height: 1.8;
       color: #1d3557; white-space: pre; }
.kb .fact { color: #0a7d33; }
.kb .rule { color: #1d3557; }
.kb .head { font-weight: 700; }
.query-row { margin-bottom: .5rem; }
.query-presets { display: flex; flex-wrap: wrap; gap: .35rem; margin: .3rem 0; }
.preset { font: 600 12px ui-monospace, monospace; padding: .25rem .55rem;
          border: 1px solid #adb5c2; background: #fff; border-radius: 5px;
          cursor: pointer; color: #1d3557; }
.preset:hover { background: #e8eef3; }
input#query { width: 100%; font: 14px ui-monospace, monospace; padding: .4rem .6rem;
              border: 1px solid #adb5c2; border-radius: 6px; margin-bottom: .4rem; }
button#run { font: 700 13px system-ui; padding: .42rem 1rem; background: #1d3557;
             color: #fff; border: none; border-radius: 7px; cursor: pointer; }
button#run:hover { background: #14253d; }
.trace { margin-top: .5rem; }
.step { padding: .35rem .6rem; border-radius: 6px; margin-bottom: .3rem;
        font-family: ui-monospace, monospace; font-size: .83rem; line-height: 1.5; }
.step-unify { background: #e8f4fd; border-left: 3px solid #2196f3; }
.step-resolve { background: #f0faf2; border-left: 3px solid #0a7d33; }
.step-fail { background: #fff0f0; border-left: 3px solid #c92f3c; color: #8a1a1a; }
.step-success { background: #e6faf0; border-left: 3px solid #0a7d33;
                font-weight: 700; color: #0a7d33; font-family: system-ui; font-size: .95rem; }
.step-false { background: #fff5f5; border-left: 3px solid #c92f3c;
              font-weight: 700; color: #c92f3c; font-family: system-ui; font-size: .95rem; }
.label { font-size: .72rem; font-weight: 700; text-transform: uppercase;
         letter-spacing: .05em; color: #5a6a7a; margin-right: .4rem; }

// Code not found

Each step either unifies a goal with the head of a clause (matching variables to concrete values) or resolves two complementary literals away. When the goal list becomes empty, the query is proved. When every branch fails, the query is false.

Resolution looks deceptively simple — one rule, repeated. But its power and limits are subtle:

• Refutation-completeness: Robinson proved that if a set of clauses is unsatisfiable, resolution will eventually find the contradiction. Nothing is missed — it is complete for refutation.
• But undecidable in general: for full first-order logic, the search space is infinite. Resolution may run forever on satisfiable inputs because there is no bound on proof length. Gödel's incompleteness result and Church's undecidability theorem guarantee this ceiling.
• Horn clauses save the day: Prolog restricts to Horn clauses — rules with at most one positive literal. This restriction enables SLD resolution (Selective Linear Definite), a deterministic depth-first strategy that is sound and complete for Horn logic and runs in time proportional to the proof length. It is no longer undecidable — but it can still loop on recursive rules that never ground out.
• Prolog's cut (!): to escape infinite loops, Prolog adds an extra-logical pruning operator. This makes full Prolog programs Turing-complete, bringing undecidability back for arbitrary programs.

The relationship to other hard problems is direct: SAT is the Boolean fragment of what resolution solves, and P vs NP asks exactly whether finding short resolution proofs is tractable.

The idea of proving by contradiction through mechanical clause combination turned out to be deeply practical:

• Logic programming: Prolog is still the canonical language for symbolic AI, natural-language parsing, constraint solving and knowledge representation.
• Automated theorem proving: theorem provers for mathematics and hardware verification (ACL2, Lean, Coq under the hood) all descend from Robinson's resolution.
• Expert systems: medical diagnosis systems like MYCIN in the 1970s used Horn-clause reasoning that is exactly SLD resolution.
• Type inference: Hindley-Milner type checking in Haskell and ML is formally equivalent to Horn-clause resolution over type constraints.
• SAT and SMT solvers: modern DPLL and CDCL solvers are resolution-based — every learned clause in a SAT solver is a resolution step. These solvers verify chips, find bugs in software and schedule flights.
• Datalog and databases: deductive databases that power graph analytics and program analysis (e.g., Datomic, Soufflé) are Horn-clause engines derived from resolution.

Robinson's resolution principle is one of the most productive ideas in the history of computing. A single rule — cancel a complementary literal, merge the rest — turned out to be all the logic you need to prove any provable first-order sentence, power an entire programming paradigm, and seed the SAT and SMT solvers that modern software verification depends on.

Its limits are equally instructive: complete for refutation yet undecidable in general, fully decidable only when restricted to Horn clauses. Understanding where resolution succeeds and where it loops forever is understanding the same boundary that P vs NP draws between what is computable and what is merely theoretically possible.