Resolution: Proof by Refutation

in progressThis lesson is still being built - content, demos, and checkpoints may change before release.

Resolution

Loading interactive demo…

The graph is the proof: the premise clauses and the negated goal across the top, and each resolvent below the two clauses it came from, with an edge from each parent. The strip below lists every clause in the set in the order it arrived. The empty clause, when it appears, is the contradiction.Take the tour, or press and explore. Legend:

The panel beside the stage is the real ResolutionProver class from the published library executing in your browser, with the current line highlighted.

A premise clause.
The negated goal and every clause descended from it: the set of support.
A resolvent of premises alone, which the set-of-support strategy never makes.
The two clauses resolving this step.
The clause just derived; the empty clause.
The tapped clause with its parents and children.

clauses counts the set so far, derived the resolvents made, tautologies the resolvents dropped for holding a variable and its negation, goal the goal and whether the empty clause was reached. Tap a clause to light its edges.

The code panel shows bare executable code by default. The bar above it names the file (hover the name for the full published path); options holds the toggles: comments, the tracer instrumentation that produces this visualization, and verbose names for the terse identifiers (display only: the default is the byte-exact published file). The view switch adds plain-English narration: both interleaves it with the code, pseudo shows only the pseudocode. hide code collapses the panel; the rail it leaves behind brings it back.

Keys: Space play/pause · ←/→ step · Home/End jump · R reset · F fullscreen · G guided tour

The rule. From $A \vee p$ and $B \vee \neg p$ conclude $A \vee B$ . Either $p$ holds, so the second clause needs $B$ , or it does not, so the first needs $A$ ; either way $A \vee B$ . The resolvent is entailed by its parents, so adding it to a set changes nothing about which assignments satisfy the set. Resolving $p$ with $\neg p$ leaves $A \vee B$ with nothing in it, the empty clause, which no assignment satisfies.

Refutation. Premises $\Gamma$ entail $\varphi$ exactly when $\Gamma \cup \{\neg\varphi\}$ is unsatisfiable. So to prove $\varphi$ , put $\neg\varphi$ into clause form, add it to the premises, and look for the empty clause. Finding it shows the set is contradictory, hence that $\varphi$ follows. Resolution cannot derive an arbitrary consequence directly; it can only find contradictions, which is enough.

Completeness. If a finite set of clauses is unsatisfiable, the empty clause is reachable by resolution. The proof is by induction on the number of variables: pick one, resolve every clause holding it against every clause holding its negation, drop both, and the result is unsatisfiable with one fewer variable. That is the Davis-Putnam procedure, and it shows the exhaustive strategy always terminates with an answer: either the empty clause or a saturated set, which then has a model.

Strategies. Breadth resolves every clashing pair in order and drowns in resolvents of the premises alone. Set of support resolves only pairs in which at least one clause descends from the negated goal; if the premises themselves are satisfiable, this is still complete, and the stage shows the chain problem shrink from about a dozen resolvents to four. Unit preference resolves a one-literal clause first, since its resolvent is shorter than the other parent. Tautologous resolvents, holding $p \vee \neg p$ , are dropped: they are true in every assignment and help nothing.

Cost. The procedure is complete but not fast. Haken showed that refuting the pigeonhole clauses for $n+1$ pigeons in $n$ holes takes exponentially many resolvents, and no strategy escapes that: it is a bound on the proof, not on the search. The SAT lesson's DPLL and its CDCL descendants are resolution with a very good search order.

Choices worth reading closely in the implementation (the code panel's comments and tracer checkboxes reveal the full published file):

Pairs are tried once: the tried set records each pair by index, so saturation is "no untried pair clashes", which is what makes the not-entailed verdict a verdict and not a timeout.
The set of support is a set of indices seeded with the negated goal's clauses and grown with every resolvent that has a supported parent; the support strategy only filters pairs by it.
A resolvent already in the set is skipped, compared as a set of literals, so the same clause from two different pairs is counted once.
The clause cap is a safety net for the library; the stage's problems saturate or refute well under it, and the trace says when a run was capped rather than saturated.

Logicians had rules of inference by the dozen, and a machine that searched proofs with all of them drowned in choices. In 1965 John Alan Robinson showed that one rule, resolution, suffices for clause form: if a set of clauses is contradictory, repeatedly resolving clashing pairs reaches the empty clause. Proving a theorem became refuting its negation, which is a search over a single rule, and the restriction strategies that followed, set of support and unit preference among them, made that search practical. Prolog's execution and modern SAT and SMT solvers are descendants.

1960Martin Davis and Hilary Putnam - A procedure for propositional satisfiability eliminates variables by resolving on them, the step resolution would generalize.source
1965John Alan Robinson - 'A Machine-Oriented Logic Based on the Resolution Principle' gives the single rule, with unification for first-order terms, and proves it refutation complete.source
1965Lawrence Wos, George Robinson and Daniel Carson - Set of support: resolve only pairs that descend from the negated goal, and completeness survives while the search shrinks.source
1972Robert Kowalski - SLD resolution, linear resolution restricted to Horn clauses, becomes the execution model of logic programming and Prolog.source
1985Armin Haken - Proves that resolution proofs of the pigeonhole principle are exponentially long, the first strong lower bound on a proof system.source

Used today

Automated theorem provers - Vampire, E, and Prover9 search for resolution refutations of first-order problems, with term orderings and indexing to tame the pair explosion.
SAT solvers - A CDCL solver's learned clauses are resolvents of the clauses along a conflict, so its proof of unsatisfiability is a resolution proof.
Prolog - Answering a query is SLD resolution: the negated query resolves against program clauses until the empty clause, and the bindings along the way are the answer.

problem

strategy

clauses: 6
derived: 3
tautologies: 0
goal: q: proved

resolution-prover.ts

import type { Tracer } from "../trace";import { complementary, dedupe, isTautologous, sameLiteral, type Clause } from "./clauses";export type ResolutionStrategy = "breadth" | "support" | "unit";export interface ResolutionStep {  left: number;  right: number;  /** The variable resolved on. */  on: string;  resolvent: Clause;  index: number;}export interface ResolutionResult {  proved: boolean;  /** Every clause in the set at the end: premises, the negated goal, and the resolvents, in index order. */  clauses: Clause[];  steps: ResolutionStep[];  /** How many clauses came from the negated goal. */  goalClauses: number;}/** The most clauses a run may hold before it stops: the stage's problems resolve long before it. */export const MAX_RESOLUTION_CLAUSES = 60;/** * Resolution refutation for propositional clauses. To prove that the * premises entail a goal, add the goal's negation to the clause set * and resolve pairs: two clauses holding a variable and its negation * combine into one holding everything else, which follows from both. * Deriving the empty clause, which nothing satisfies, shows the set * is contradictory, so the goal was entailed; a set that stops * producing new clauses without it does not entail the goal. One rule * replaces every inference rule of the truth-table lessons, and it is * complete: if the goal follows, the empty clause is reachable. The * strategy orders the pairs: breadth first over the set, set of * support (one parent must descend from the negated goal), or unit * preference (a one-literal parent first). * * Time: exponential in the worst case. Space: O(clauses). */export class ResolutionProver {  constructor(    private readonly tracer?: Tracer,    private readonly strategy: ResolutionStrategy = "breadth",  ) {}  entails(premises: readonly Clause[], negatedGoal: readonly Clause[]): ResolutionResult {    const clauses: Clause[] = premises.map(dedupe);    const sos = new Set<number>();    const setOfSupport = new Set<number>();    negatedGoal.forEach((clause) => {      clauses.push(dedupe(clause));      sos.add(clauses.length - 1);      setOfSupport.add(clauses.length - 1);      // ▸ assume the opposite of the goal, as a clause      this.tracer?.emit("negate-goal", { index: clauses.length - 1, clause: clauses[clauses.length - 1]!.map((l) => ({ ...l })), count: negatedGoal.length });    });    const steps: ResolutionStep[] = [];    const tried = new Set<string>();    const triedPairs = new Set<string>();    for (;;) {      const pair = this.nextPair(clauses, tried, sos);      const pair = this.nextPair(clauses, triedPairs, setOfSupport);      if (!pair) break;      const [i, j] = pair;      tried.add(`${i},${j}`);      triedPairs.add(`${i},${j}`);      const a = clauses[i]!;      const b = clauses[j]!;      for (const literal of a) {        const match = b.find((other) => complementary(literal, other));        if (!match) continue;        const resolvent = dedupe([...a.filter((l) => !sameLiteral(l, literal)), ...b.filter((l) => !sameLiteral(l, match))]);        if (isTautologous(resolvent)) {          // ▸ the new clause holds a variable and its negation, so it says nothing          this.tracer?.emit("tautology", { left: i, right: j, on: literal.name, resolvent: resolvent.map((l) => ({ ...l })) });          continue;        }        if (clauses.some((c) => ResolutionProver.same(c, resolvent))) continue;        clauses.push(resolvent);        const index = clauses.length - 1;        if (sos.has(i) || sos.has(j)) sos.add(index);        if (setOfSupport.has(i) || setOfSupport.has(j)) setOfSupport.add(index);        steps.push({ left: i, right: j, on: literal.name, resolvent, index });        // ▸ two clauses clash on a variable: the rest of both make a new clause        this.tracer?.emit("resolve", { left: i, right: j, on: literal.name, resolvent: resolvent.map((l) => ({ ...l })), index, clauses: clauses.length });        if (resolvent.length === 0) {          // ▸ the empty clause: the set is contradictory, the goal follows          this.tracer?.emit("empty-clause", { index, steps: steps.length, clauses: clauses.length });          return { proved: true, clauses, steps, goalClauses: negatedGoal.length };        }        if (clauses.length >= MAX_RESOLUTION_CLAUSES) break;      }      if (clauses.length >= MAX_RESOLUTION_CLAUSES) break;    }    // ▸ no new clause can be made: the goal does not follow    this.tracer?.emit("saturated", { clauses: clauses.length, steps: steps.length, capped: clauses.length >= MAX_RESOLUTION_CLAUSES });    return { proved: false, clauses, steps, goalClauses: negatedGoal.length };  }  /** The next untried pair the strategy allows: the earliest by the later clause, units first for unit preference. */  private nextPair(clauses: readonly Clause[], tried: ReadonlySet<string>, sos: ReadonlySet<number>): [number, number] | null {  private nextPair(clauses: readonly Clause[], triedPairs: ReadonlySet<string>, setOfSupport: ReadonlySet<number>): [number, number] | null {    const allowed = (i: number, j: number): boolean => {      if (tried.has(`${i},${j}`)) return false;      if (triedPairs.has(`${i},${j}`)) return false;      if (this.strategy === "support" && !sos.has(i) && !sos.has(j)) return false;      if (this.strategy === "support" && !setOfSupport.has(i) && !setOfSupport.has(j)) return false;      return clauses[i]!.some((l) => clauses[j]!.some((o) => complementary(l, o)));    };    if (this.strategy === "unit") {      for (let j = 1; j < clauses.length; j++) for (let i = 0; i < j; i++) if ((clauses[i]!.length === 1 || clauses[j]!.length === 1) && allowed(i, j)) return [i, j];    }    for (let j = 1; j < clauses.length; j++) for (let i = 0; i < j; i++) if (allowed(i, j)) return [i, j];    return null;  }  private static same(a: Clause, b: Clause): boolean {    return a.length === b.length && a.every((l) => b.some((o) => sameLiteral(l, o)));  }}

clauses =: 6
steps =: 3
proved =: yes

Proved: q follows, since adding its negation gave a contradiction in 3 resolutions over 6 clauses.

import type { Tracer } from "../trace";import { complementary, dedupe, isTautologous, sameLiteral, type Clause } from "./clauses";export type ResolutionStrategy = "breadth" | "support" | "unit";export interface ResolutionStep { left: number; right: number; /** The variable resolved on. */ on: string; resolvent: Clause; index: number;}export interface ResolutionResult { proved: boolean; /** Every clause in the set at the end: premises, the negated goal, and the resolvents, in index order. */ clauses: Clause[]; steps: ResolutionStep[]; /** How many clauses came from the negated goal. */ goalClauses: number;}/** The most clauses a run may hold before it stops: the stage's problems resolve long before it. */export const MAX_RESOLUTION_CLAUSES = 60;/** * Resolution refutation for propositional clauses. To prove that the * premises entail a goal, add the goal's negation to the clause set * and resolve pairs: two clauses holding a variable and its negation * combine into one holding everything else, which follows from both. * Deriving the empty clause, which nothing satisfies, shows the set * is contradictory, so the goal was entailed; a set that stops * producing new clauses without it does not entail the goal. One rule * replaces every inference rule of the truth-table lessons, and it is * complete: if the goal follows, the empty clause is reachable. The * strategy orders the pairs: breadth first over the set, set of * support (one parent must descend from the negated goal), or unit * preference (a one-literal parent first). * * Time: exponential in the worst case. Space: O(clauses). */export class ResolutionProver { constructor( private readonly tracer?: Tracer, private readonly strategy: ResolutionStrategy = "breadth", ) {} entails(premises: readonly Clause[], negatedGoal: readonly Clause[]): ResolutionResult { const clauses: Clause[] = premises.map(dedupe); const sos = new Set<number>(); const setOfSupport = new Set<number>(); negatedGoal.forEach((clause) => { clauses.push(dedupe(clause)); sos.add(clauses.length - 1); setOfSupport.add(clauses.length - 1); // ▸ assume the opposite of the goal, as a clause this.tracer?.emit("negate-goal", { index: clauses.length - 1, clause: clauses[clauses.length - 1]!.map((l) => ({ ...l })), count: negatedGoal.length }); }); const steps: ResolutionStep[] = []; const tried = new Set<string>(); const triedPairs = new Set<string>(); for (;;) { const pair = this.nextPair(clauses, tried, sos); const pair = this.nextPair(clauses, triedPairs, setOfSupport); if (!pair) break; const [i, j] = pair; tried.add(`${i},${j}`); triedPairs.add(`${i},${j}`); const a = clauses[i]!; const b = clauses[j]!; for (const literal of a) { const match = b.find((other) => complementary(literal, other)); if (!match) continue; const resolvent = dedupe([...a.filter((l) => !sameLiteral(l, literal)), ...b.filter((l) => !sameLiteral(l, match))]); if (isTautologous(resolvent)) { // ▸ the new clause holds a variable and its negation, so it says nothing this.tracer?.emit("tautology", { left: i, right: j, on: literal.name, resolvent: resolvent.map((l) => ({ ...l })) }); continue; } if (clauses.some((c) => ResolutionProver.same(c, resolvent))) continue; clauses.push(resolvent); const index = clauses.length - 1; if (sos.has(i) || sos.has(j)) sos.add(index); if (setOfSupport.has(i) || setOfSupport.has(j)) setOfSupport.add(index); steps.push({ left: i, right: j, on: literal.name, resolvent, index }); // ▸ two clauses clash on a variable: the rest of both make a new clause this.tracer?.emit("resolve", { left: i, right: j, on: literal.name, resolvent: resolvent.map((l) => ({ ...l })), index, clauses: clauses.length }); if (resolvent.length === 0) { // ▸ the empty clause: the set is contradictory, the goal follows this.tracer?.emit("empty-clause", { index, steps: steps.length, clauses: clauses.length }); return { proved: true, clauses, steps, goalClauses: negatedGoal.length }; } if (clauses.length >= MAX_RESOLUTION_CLAUSES) break; } if (clauses.length >= MAX_RESOLUTION_CLAUSES) break; } // ▸ no new clause can be made: the goal does not follow this.tracer?.emit("saturated", { clauses: clauses.length, steps: steps.length, capped: clauses.length >= MAX_RESOLUTION_CLAUSES }); return { proved: false, clauses, steps, goalClauses: negatedGoal.length }; } /** The next untried pair the strategy allows: the earliest by the later clause, units first for unit preference. */ private nextPair(clauses: readonly Clause[], tried: ReadonlySet<string>, sos: ReadonlySet<number>): [number, number] | null { private nextPair(clauses: readonly Clause[], triedPairs: ReadonlySet<string>, setOfSupport: ReadonlySet<number>): [number, number] | null { const allowed = (i: number, j: number): boolean => { if (tried.has(`${i},${j}`)) return false; if (triedPairs.has(`${i},${j}`)) return false; if (this.strategy === "support" && !sos.has(i) && !sos.has(j)) return false; if (this.strategy === "support" && !setOfSupport.has(i) && !setOfSupport.has(j)) return false; return clauses[i]!.some((l) => clauses[j]!.some((o) => complementary(l, o))); }; if (this.strategy === "unit") { for (let j = 1; j < clauses.length; j++) for (let i = 0; i < j; i++) if ((clauses[i]!.length === 1 || clauses[j]!.length === 1) && allowed(i, j)) return [i, j]; } for (let j = 1; j < clauses.length; j++) for (let i = 0; i < j; i++) if (allowed(i, j)) return [i, j]; return null; } private static same(a: Clause, b: Clause): boolean { return a.length === b.length && a.every((l) => b.some((o) => sameLiteral(l, o))); }}