Introduction to Resolution and Prolog

Introduction

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.

Try It

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">A small family knowledge base. Each fact or rule is a <b>clause</b>. Click <b>Run query</b> to watch unification and resolution chain to an answer.</p>
<div class="kb-area">
  <div class="kb-label">Knowledge base (facts & rules)</div>
  <div id="kb" class="kb"></div>
</div>
<div class="query-row">
  <label class="kb-label" for="query">Query</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 query</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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ── Knowledge base ─────────────────────────────────────────────────────────
// Clauses are represented as { head: Term | null, body: Term[] }
// A fact  has body=[]. A rule has body.length >= 1.
// null head = goal clause (used internally).
// Terms: { name: string, args: Term[] }  (constants: args=[])

const KB_TEXT = [
  'parent(tom, bob)',
  'parent(tom, liz)',
  'parent(bob, ann)',
  'parent(bob, pat)',
  'ancestor(X, Y) :- parent(X, Y)',
  'ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y)',
];

// ── Parser ──────────────────────────────────────────────────────────────────
function parseTerm(s) {
  s = s.trim();
  const m = s.match(/^([A-Za-z_][A-Za-z0-9_]*)\((.+)\)$/);
  if (m) return { name: m[1], args: splitArgs(m[2]).map(parseTerm) };
  return { name: s, args: [] };
}
function splitArgs(s) {
  const parts = []; let depth = 0, cur = '';
  for (const ch of s) {
    if (ch === '(' ) depth++;
    if (ch === ')' ) depth--;
    if (ch === ',' && depth === 0) { parts.push(cur.trim()); cur = ''; }
    else cur += ch;
  }
  if (cur.trim()) parts.push(cur.trim());
  return parts;
}
function parseClause(s) {
  s = s.trim();
  const idx = s.indexOf(':-');
  if (idx === -1) return { head: parseTerm(s), body: [] };
  const head = parseTerm(s.slice(0, idx).trim());
  const body = splitArgs(s.slice(idx + 2)).map(b => parseTerm(b.trim()));
  return { head, body };
}
function termStr(t) {
  if (!t.args.length) return t.name;
  return t.name + '(' + t.args.map(termStr).join(', ') + ')';
}
function isVar(t) { return t.args.length === 0 && /^[A-Z_]/.test(t.name); }

// ── Substitution / Unification ──────────────────────────────────────────────
function applySubst(t, subst) {
  if (isVar(t)) {
    if (subst[t.name] !== undefined) return applySubst(subst[t.name], subst);
    return t;
  }
  return { name: t.name, args: t.args.map(a => applySubst(a, subst)) };
}
function occursIn(varName, t, subst) {
  t = applySubst(t, subst);
  if (isVar(t)) return t.name === varName;
  return t.args.some(a => occursIn(varName, a, subst));
}
function unify(t1, t2, subst) {
  t1 = applySubst(t1, subst); t2 = applySubst(t2, subst);
  if (isVar(t1)) {
    if (t1.name === t2.name && isVar(t2)) return { ...subst };
    if (occursIn(t1.name, t2, subst)) return null;
    return { ...subst, [t1.name]: t2 };
  }
  if (isVar(t2)) return unify(t2, t1, subst);
  if (t1.name !== t2.name || t1.args.length !== t2.args.length) return null;
  for (let i = 0; i < t1.args.length; i++) {
    subst = unify(t1.args[i], t2.args[i], subst);
    if (subst === null) return null;
  }
  return subst;
}

// ── Variable renaming (to avoid clashes between resolution steps) ───────────
let varCounter = 0;
function freshClause(clause) {
  const id = varCounter++;
  const vars = {};
  function rename(t) {
    if (isVar(t)) {
      if (!vars[t.name]) vars[t.name] = { name: t.name + '_' + id, args: [] };
      return vars[t.name];
    }
    return { name: t.name, args: t.args.map(rename) };
  }
  return {
    head: clause.head ? rename(clause.head) : null,
    body: clause.body.map(rename),
  };
}

// ── SLD Resolution (depth-first, depth-limited) ──────────────────────────────
const MAX_DEPTH = 30;
function solve(goals, subst, kb, steps, depth) {
  if (depth > MAX_DEPTH) { steps.push({ type: 'fail', msg: 'Depth limit reached — possible infinite loop.' }); return false; }
  if (goals.length === 0) return true;
  const [goal, ...rest] = goals;
  const resolvedGoal = applySubst(goal, subst);
  for (const raw of kb) {
    const clause = freshClause(raw);
    const s2 = unify(resolvedGoal, clause.head, subst);
    if (s2 === null) continue;
    const newGoals = [...clause.body.map(b => applySubst(b, s2)), ...rest];
    steps.push({
      type: 'unify',
      msg: fmt('Unify %termStr%  with  %termStr2%%v%', { termStr: termStr(resolvedGoal), termStr2: termStr(clause.head), v: clause.body.length ? '  →  body: ' + clause.body.map(termStr).join(', ') : '  →  fact ✓' }),
    });
    if (solve(newGoals, s2, kb, steps, depth + 1)) {
      Object.assign(subst, s2);
      return true;
    }
  }
  steps.push({ type: 'fail', msg: fmt('No clause unifies with %termStr% — backtrack.', { termStr: termStr(resolvedGoal) }) });
  return false;
}

// ── Render knowledge base ───────────────────────────────────────────────────
const kb = KB_TEXT.map(parseClause);
function renderKB() {
  const el = document.getElementById('kb');
  el.innerHTML = KB_TEXT.map(line => {
    const cls = line.includes(':-') ? 'rule' : 'fact';
    return '<span class="' + cls + '">' + line + '</span>';
  }).join('\n');
}

// ── Run ─────────────────────────────────────────────────────────────────────
function run() {
  const qText = document.getElementById('query').value.trim();
  if (!qText) return;
  varCounter = 0;
  const steps = [];
  let goal;
  try { goal = parseTerm(qText); } catch(e) { return; }
  const subst = {};
  const proved = solve([goal], subst, kb, steps, 0);
  const trace = document.getElementById('trace');
  trace.innerHTML = '';
  steps.forEach(s => {
    const div = document.createElement('div');
    div.className = 'step step-' + s.type;
    const lbl = { unify: 'Unify', resolve: 'Resolve', fail: 'Backtrack' }[s.type] || '';
    div.innerHTML = lbl ? '<span class="label">' + lbl + '</span>' + s.msg : s.msg;
    trace.appendChild(div);
  });
  const result = document.createElement('div');
  result.className = proved ? 'step step-success' : 'step step-false';
  result.textContent = proved ? fmt('✓ true — %qText% is provable.', { qText: qText }) : fmt('✗ false — %qText% is not provable.', { qText: qText });
  trace.appendChild(result);
  console.log(proved ? 'PROVED' : 'FAILED', qText, '| steps:', steps.length);
}

document.getElementById('run').addEventListener('click', run);
document.querySelectorAll('.preset').forEach(btn => {
  btn.addEventListener('click', () => {
    document.getElementById('query').value = btn.dataset.q;
    run();
  });
});
renderKB();
run();

<p class="hint">A small family knowledge base. Each fact or rule is a <b>clause</b>. Click <b>Run query</b> to watch unification and resolution chain to an answer.</p>
<div class="kb-area">
  <div class="kb-label">Knowledge base (facts & rules)</div>
  <div id="kb" class="kb"></div>
</div>
<div class="query-row">
  <label class="kb-label" for="query">Query</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 query</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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ── Knowledge base ─────────────────────────────────────────────────────────
// Clauses are represented as { head: Term | null, body: Term[] }
// A fact  has body=[]. A rule has body.length >= 1.
// null head = goal clause (used internally).
// Terms: { name: string, args: Term[] }  (constants: args=[])

const KB_TEXT = [
  'parent(tom, bob)',
  'parent(tom, liz)',
  'parent(bob, ann)',
  'parent(bob, pat)',
  'ancestor(X, Y) :- parent(X, Y)',
  'ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y)',
];

// ── Parser ──────────────────────────────────────────────────────────────────
function parseTerm(s) {
  s = s.trim();
  const m = s.match(/^([A-Za-z_][A-Za-z0-9_]*)\((.+)\)$/);
  if (m) return { name: m[1], args: splitArgs(m[2]).map(parseTerm) };
  return { name: s, args: [] };
}
function splitArgs(s) {
  const parts = []; let depth = 0, cur = '';
  for (const ch of s) {
    if (ch === '(' ) depth++;
    if (ch === ')' ) depth--;
    if (ch === ',' && depth === 0) { parts.push(cur.trim()); cur = ''; }
    else cur += ch;
  }
  if (cur.trim()) parts.push(cur.trim());
  return parts;
}
function parseClause(s) {
  s = s.trim();
  const idx = s.indexOf(':-');
  if (idx === -1) return { head: parseTerm(s), body: [] };
  const head = parseTerm(s.slice(0, idx).trim());
  const body = splitArgs(s.slice(idx + 2)).map(b => parseTerm(b.trim()));
  return { head, body };
}
function termStr(t) {
  if (!t.args.length) return t.name;
  return t.name + '(' + t.args.map(termStr).join(', ') + ')';
}
function isVar(t) { return t.args.length === 0 && /^[A-Z_]/.test(t.name); }

// ── Substitution / Unification ──────────────────────────────────────────────
function applySubst(t, subst) {
  if (isVar(t)) {
    if (subst[t.name] !== undefined) return applySubst(subst[t.name], subst);
    return t;
  }
  return { name: t.name, args: t.args.map(a => applySubst(a, subst)) };
}
function occursIn(varName, t, subst) {
  t = applySubst(t, subst);
  if (isVar(t)) return t.name === varName;
  return t.args.some(a => occursIn(varName, a, subst));
}
function unify(t1, t2, subst) {
  t1 = applySubst(t1, subst); t2 = applySubst(t2, subst);
  if (isVar(t1)) {
    if (t1.name === t2.name && isVar(t2)) return { ...subst };
    if (occursIn(t1.name, t2, subst)) return null;
    return { ...subst, [t1.name]: t2 };
  }
  if (isVar(t2)) return unify(t2, t1, subst);
  if (t1.name !== t2.name || t1.args.length !== t2.args.length) return null;
  for (let i = 0; i < t1.args.length; i++) {
    subst = unify(t1.args[i], t2.args[i], subst);
    if (subst === null) return null;
  }
  return subst;
}

// ── Variable renaming (to avoid clashes between resolution steps) ───────────
let varCounter = 0;
function freshClause(clause) {
  const id = varCounter++;
  const vars = {};
  function rename(t) {
    if (isVar(t)) {
      if (!vars[t.name]) vars[t.name] = { name: t.name + '_' + id, args: [] };
      return vars[t.name];
    }
    return { name: t.name, args: t.args.map(rename) };
  }
  return {
    head: clause.head ? rename(clause.head) : null,
    body: clause.body.map(rename),
  };
}

// ── SLD Resolution (depth-first, depth-limited) ──────────────────────────────
const MAX_DEPTH = 30;
function solve(goals, subst, kb, steps, depth) {
  if (depth > MAX_DEPTH) { steps.push({ type: 'fail', msg: 'Depth limit reached — possible infinite loop.' }); return false; }
  if (goals.length === 0) return true;
  const [goal, ...rest] = goals;
  const resolvedGoal = applySubst(goal, subst);
  for (const raw of kb) {
    const clause = freshClause(raw);
    const s2 = unify(resolvedGoal, clause.head, subst);
    if (s2 === null) continue;
    const newGoals = [...clause.body.map(b => applySubst(b, s2)), ...rest];
    steps.push({
      type: 'unify',
      msg: fmt('Unify %termStr%  with  %termStr2%%v%', { termStr: termStr(resolvedGoal), termStr2: termStr(clause.head), v: clause.body.length ? '  →  body: ' + clause.body.map(termStr).join(', ') : '  →  fact ✓' }),
    });
    if (solve(newGoals, s2, kb, steps, depth + 1)) {
      Object.assign(subst, s2);
      return true;
    }
  }
  steps.push({ type: 'fail', msg: fmt('No clause unifies with %termStr% — backtrack.', { termStr: termStr(resolvedGoal) }) });
  return false;
}

// ── Render knowledge base ───────────────────────────────────────────────────
const kb = KB_TEXT.map(parseClause);
function renderKB() {
  const el = document.getElementById('kb');
  el.innerHTML = KB_TEXT.map(line => {
    const cls = line.includes(':-') ? 'rule' : 'fact';
    return '<span class="' + cls + '">' + line + '</span>';
  }).join('\n');
}

// ── Run ─────────────────────────────────────────────────────────────────────
function run() {
  const qText = document.getElementById('query').value.trim();
  if (!qText) return;
  varCounter = 0;
  const steps = [];
  let goal;
  try { goal = parseTerm(qText); } catch(e) { return; }
  const subst = {};
  const proved = solve([goal], subst, kb, steps, 0);
  const trace = document.getElementById('trace');
  trace.innerHTML = '';
  steps.forEach(s => {
    const div = document.createElement('div');
    div.className = 'step step-' + s.type;
    const lbl = { unify: 'Unify', resolve: 'Resolve', fail: 'Backtrack' }[s.type] || '';
    div.innerHTML = lbl ? '<span class="label">' + lbl + '</span>' + s.msg : s.msg;
    trace.appendChild(div);
  });
  const result = document.createElement('div');
  result.className = proved ? 'step step-success' : 'step step-false';
  result.textContent = proved ? fmt('✓ true — %qText% is provable.', { qText: qText }) : fmt('✗ false — %qText% is not provable.', { qText: qText });
  trace.appendChild(result);
  console.log(proved ? 'PROVED' : 'FAILED', qText, '| steps:', steps.length);
}

document.getElementById('run').addEventListener('click', run);
document.querySelectorAll('.preset').forEach(btn => {
  btn.addEventListener('click', () => {
    document.getElementById('query').value = btn.dataset.q;
    run();
  });
});
renderKB();
run();

Result

Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Comments

Loading comments...

https://www.kipuhub.com/en/article/resolution-prolog/Content licensed under CC BY-NC 4.0.

Cookies & privacy

Resolution and Prolog

The inference engine that proves by contradiction