Proof Complexity

Introduction

Suppose you want to convince someone that a logic formula has no satisfying assignment — that it's a tautology in negation, or equivalently that its negation is unsatisfiable. You write down a proof. How long does that proof have to be?

For simple cases the answer is short. But for carefully chosen formulas, every proof in a given system must be exponentially long — no matter how clever the strategy. That is the central discovery of proof complexity: some true statements are hard to certify, not just hard to discover.

The field was born in 1979 when Stephen Cook and Robert Reckhow formalized the question. They showed that proving NP ≠ co-NP is equivalent to showing that no proof system can always produce short proofs of tautologies. So proof complexity is not just about logic — it sits at the heart of the deepest open problem in computer science.

Build a Resolution Proof

Resolution is the simplest proof system for unsatisfiability. Its one rule: from clause $(A \lor x)$ and clause $(B \lor \neg x)$ derive $(A \lor B)$ — the resolvent. A refutation is a resolution proof that derives the empty clause $\bot$ , showing the formula is unsatisfiable.

<p class="hint">
  Resolution derives new clauses by canceling complementary literals. From clause
      <i>(A&nbsp;∨&nbsp;x)</i> and <i>(B&nbsp;∨&nbsp;¬x)</i> you derive the resolvent
      <i>(A&nbsp;∨&nbsp;B)</i>. A <b>refutation</b> derives the empty clause ⊥,
      proving the formula is unsatisfiable. Step through the proof to see how length grows.
</p>
<div class="controls">
  <label for="formula-select">Formula:</label>
  <select id="formula-select">
    <option value="0">PHP(2,1) — 2 pigeons, 1 hole (4 steps)</option>
    <option value="1">PHP(3,2) — 3 pigeons, 2 holes (12 steps)</option>
    <option value="2">2-CNF clash — all four (x,y) combinations (6 steps)</option>
  </select>
</div>
<div class="proof-area">
  <div class="clause-list" id="clause-list"></div>
</div>
<div class="step-info" id="step-info">Press "Next Step" to begin the refutation.</div>
<div class="btns">
  <button id="btn-prev" type="button" class="ghost" disabled>← Prev</button>
  <button id="btn-next" type="button">Next Step →</button>
  <button id="btn-all" type="button" class="ghost">Show All</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="stats" id="stats"></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 .6rem; line-height: 1.45; }
.controls { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; flex-wrap: wrap; }
label { font-weight: 600; font-size: .88rem; }
select { font-size: .88rem; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px;
         background: #f5f7fa; cursor: pointer; }
.proof-area { border: 1px solid #cdd9e3; border-radius: 8px; background: #f8fafc;
              padding: .5rem .7rem; min-height: 120px; max-height: 220px; overflow-y: auto;
              margin-bottom: .5rem; }
.clause-list { display: flex; flex-direction: column; gap: 3px; }
.clause-row { display: flex; align-items: baseline; gap: .5rem; font-size: .85rem;
              padding: 2px 0; }
.clause-row.axiom  { color: #1d3557; }
.clause-row.derived { color: #0a7d33; }
.clause-row.empty-clause { color: #c92f3c; font-weight: 700; }
.clause-row.new { animation: fadeIn .3s ease; }
@keyframes fadeIn { from { opacity: 0; transform: translateY(-4px); } to { opacity: 1; } }
.row-num { color: #888; font-size: .75rem; min-width: 24px; text-align: right; flex-shrink: 0; }
.clause-text { font-family: ui-monospace, monospace; }
.justification { color: #777; font-size: .75rem; font-style: italic; }
.step-info { font-size: .9rem; font-weight: 600; margin: .4rem 0; min-height: 1.4em;
             color: #1d3557; }
.btns { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .4rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .8rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .4; cursor: not-allowed; }
.stats { font-size: .82rem; color: #555; min-height: 1.2em; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Resolution proof demo for three unsatisfiable propositional formulas.
//
// Literal encoding: positive literal = string like ’p11’; negative = ’¬p11’.
// Resolution rule: from (A ∨ x) and (B ∨ ¬x) derive the resolvent (A ∨ B).
// A resolution REFUTATION is a sequence of clauses, each an axiom or resolvent
    // of two earlier clauses, ending with the empty clause ⊥.
//
// Formula 0: PHP(2,1) — Pigeonhole principle: 2 pigeons, 1 hole.
//   Variables p11, p21. Axioms: (p11), (p21), (¬p11 ∨ ¬p21).
//   Resolution refutation in 2 derived steps (4 total).
//
// Formula 1: PHP(3,2) — Pigeonhole principle: 3 pigeons, 2 holes.
//   Variables pij. Axioms: pigeon-must-go-somewhere (A), no-sharing (B).
//   Resolution refutation in 12 derived steps (21 total).
//
// Formula 2: 2-CNF full clash on two variables x, y.
//   Clauses: (x ∨ y), (x ∨ ¬y), (¬x ∨ y), (¬x ∨ ¬y).
//   Clearly unsat (covers all 4 assignments). Refutation in 3 derived steps (7 total).
//   Shows how a Frege-style system (or extended resolution) can be shorter.

function negLit(l) { return l.startsWith('¬') ? l.slice(1) : '¬' + l; }

// Verify that child is a valid resolvent of c1 and c2
function isValidResolvent(c1, c2, child) {
  for (const l of c1) {
    const nl = negLit(l);
    if (c2.includes(nl)) {
      const res = [...c1.filter(x => x !== l), ...c2.filter(x => x !== nl)];
      const seen = new Set();
      const uniq = res.filter(x => { if (seen.has(x)) return false; seen.add(x); return true; });
      const cs = new Set(child); const es = new Set(uniq);
      if (cs.size === es.size && [...cs].every(x => es.has(x))) return true;
    }
  }
  return false;
}

function buildProof(formulaIdx) {
  const steps = [];
  function addAxiom(lits, just) {
    steps.push({ lits, type: 'axiom', just });
    return steps.length - 1;
  }
  function addStep(lits, just, p1, p2) {
    if (!isValidResolvent(steps[p1].lits, steps[p2].lits, lits)) {
      console.error(fmt('Invalid resolvent at step %length%%v%', { length: steps.length, v: 1 }),
        steps[p1].lits, '+', steps[p2].lits, '->', lits);
    }
    steps.push({ lits, type: lits.length === 0 ? 'empty-clause' : 'derived', just, parents: [p1, p2] });
    return steps.length - 1;
  }

  if (formulaIdx === 0) {
    // PHP(2,1): 2 pigeons, 1 hole
    // A-clauses: pigeon i must go in hole 1
    const a1 = addAxiom(['p11'], 'Axiom: pigeon 1 must go in hole 1');
    const a2 = addAxiom(['p21'], 'Axiom: pigeon 2 must go in hole 1');
    // B-clause: hole 1 can hold at most one pigeon
    const b  = addAxiom(['¬p11', '¬p21'], 'Axiom: hole 1 holds at most 1 pigeon');
    // Resolution refutation:
    const s1 = addStep(['¬p21'], 'Res(1, 3) on p11 — pigeon 2 out of hole 1', a1, b);
    addStep([], 'Res(2, 4) on p21 → ⊥ contradiction', a2, s1);

  } else if (formulaIdx === 1) {
    // PHP(3,2): 3 pigeons, 2 holes
    // A-axioms: 0=(p11∨p12), 1=(p21∨p22), 2=(p31∨p32)
    addAxiom(['p11', 'p12'], 'Axiom: pigeon 1 in hole 1 or 2');
    addAxiom(['p21', 'p22'], 'Axiom: pigeon 2 in hole 1 or 2');
    addAxiom(['p31', 'p32'], 'Axiom: pigeon 3 in hole 1 or 2');
    // B-axioms hole 1: 3=(¬p11∨¬p21), 4=(¬p11∨¬p31), 5=(¬p21∨¬p31)
    addAxiom(['¬p11', '¬p21'], 'Axiom: hole 1 holds at most 1 (pigeons 1,2)');
    addAxiom(['¬p11', '¬p31'], 'Axiom: hole 1 holds at most 1 (pigeons 1,3)');
    addAxiom(['¬p21', '¬p31'], 'Axiom: hole 1 holds at most 1 (pigeons 2,3)');
    // B-axioms hole 2: 6=(¬p12∨¬p22), 7=(¬p12∨¬p32), 8=(¬p22∨¬p32)
    addAxiom(['¬p12', '¬p22'], 'Axiom: hole 2 holds at most 1 (pigeons 1,2)');
    addAxiom(['¬p12', '¬p32'], 'Axiom: hole 2 holds at most 1 (pigeons 1,3)');
    addAxiom(['¬p22', '¬p32'], 'Axiom: hole 2 holds at most 1 (pigeons 2,3)');
    // 12-step resolution refutation (all verified):
    const s1  = addStep(['p12', '¬p21'], 'Res(1,4) on p11', 0, 3);
    const s2  = addStep(['p12', 'p22'],  'Res(s1,2) on p21', s1, 1);
    const s3  = addStep(['p12', '¬p31'], 'Res(1,5) on p11', 0, 4);
    const s4  = addStep(['p12', 'p32'],  'Res(s3,3) on p31', s3, 2);
    const s5  = addStep(['p22', '¬p32'], 'Res(s2,8) on p12', s2, 7);
    const s6  = addStep(['p22', 'p31'],  'Res(s5,3) on p32', s5, 2);
    const s7  = addStep(['p22', '¬p21'], 'Res(s6,6) on p31', s6, 5);
    const s8  = addStep(['p22'],          'Res(s7,2) on p21', s7, 1);
    const s9  = addStep(['¬p32'],         'Res(s8,9) on p22', s8, 8);
    const s10 = addStep(['p12'],          'Res(s4,s9) on p32', s4, s9);
    const s11 = addStep(['¬p12'],         'Res(s8,7) on p22', s8, 6);
    addStep([], 'Res(s10,s11) on p12 → ⊥', s10, s11);

  } else {
    // 2-CNF full clash: (x∨y) ∧ (x∨¬y) ∧ (¬x∨y) ∧ (¬x∨¬y)
    // Unsatisfiable: every truth assignment falsifies at least one clause.
    addAxiom(['x', 'y'],   'Axiom: (x ∨ y)');
    addAxiom(['x', '¬y'],  'Axiom: (x ∨ ¬y)');
    addAxiom(['¬x', 'y'],  'Axiom: (¬x ∨ y)');
    addAxiom(['¬x', '¬y'], 'Axiom: (¬x ∨ ¬y)');
    // Refutation in 3 steps:
    // (x∨y) + (x∨¬y) resolve on y -> (x)
    const s1 = addStep(['x'],  'Res(1,2) on y — x must be true', 0, 1);
    // (¬x∨y) + (¬x∨¬y) resolve on y -> (¬x)
    const s2 = addStep(['¬x'], 'Res(3,4) on y — x must be false', 2, 3);
    // (x) + (¬x) -> ⊥
    addStep([], 'Res(s1,s2) on x → ⊥ (x can’t be both true and false)', s1, s2);
  }
  return steps;
}

// ── State ────────────────────────────────────────────────────────────────────
let allSteps = [];
let shownCount = 0;

function loadFormula(idx) {
  allSteps = buildProof(Number(idx));
  shownCount = 0;
  renderList();
  updateInfo('Press "Next Step" to begin the refutation.');
  updateStats();
  updateButtons();
}

function fmtLits(lits) {
  if (lits.length === 0) return '⊥';
  return '(' + lits.join(' ∨ ') + ')';
}

function renderList() {
  const list = document.getElementById('clause-list');
  list.innerHTML = '';
  for (let i = 0; i < shownCount; i++) {
    const s = allSteps[i];
    const row = document.createElement('div');
    row.className = 'clause-row ' + s.type + (i === shownCount - 1 ? ' new' : '');
    row.innerHTML =
      '<span class="row-num">' + (i + 1) + '.</span>' +
      '<span class="clause-text">' + escHtml(fmtLits(s.lits)) + '</span>' +
      '<span class="justification">' + escHtml(s.just) + '</span>';
    list.appendChild(row);
  }
  document.querySelector('.proof-area').scrollTop = 9999;
}

function updateInfo(msg) {
  document.getElementById('step-info').textContent = msg;
}

function updateStats() {
  const axiomCount = allSteps.filter(s => s.type === 'axiom').length;
  const derivedShown = Math.max(0, shownCount - axiomCount);
  document.getElementById('stats').textContent =
    fmt('Axioms: %axiomCount% | Derived steps shown: %derivedShown% | Total proof length: %length% steps', { axiomCount: axiomCount, derivedShown: derivedShown, length: allSteps.length });
}

function updateButtons() {
  document.getElementById('btn-prev').disabled = shownCount <= 0;
  document.getElementById('btn-next').disabled = shownCount >= allSteps.length;
  document.getElementById('btn-all').disabled = shownCount >= allSteps.length;
}

function stepNext() {
  if (shownCount >= allSteps.length) return;
  shownCount++;
  const s = allSteps[shownCount - 1];
  renderList();
  if (s.type === 'axiom') {
    updateInfo(fmt('Axiom %shownCount%: %fmtLits%', { shownCount: shownCount, fmtLits: fmtLits(s.lits) }));
  } else if (s.type === 'empty-clause') {
    updateInfo(fmt('⊥ derived — refutation complete in %length% total steps!', { length: allSteps.length }));
  } else {
    updateInfo(fmt('Step %shownCount%: %just% → %fmtLits%', { shownCount: shownCount, just: s.just, fmtLits: fmtLits(s.lits) }));
  }
  updateStats();
  updateButtons();
}

function stepPrev() {
  if (shownCount <= 0) return;
  shownCount--;
  renderList();
  updateInfo(shownCount === 0
    ? 'Press "Next Step" to begin the refutation.'
    : fmt('Step %shownCount%: %fmtLits%', { shownCount: shownCount, fmtLits: fmtLits(allSteps[shownCount - 1].lits) }));
  updateStats();
  updateButtons();
}

function showAll() {
  shownCount = allSteps.length;
  renderList();
  updateInfo(fmt('Full proof shown — %length% total steps, ending in ⊥.', { length: allSteps.length }));
  updateStats();
  updateButtons();
}

function escHtml(s) {
  return s.replace(/&/g,'&amp;').replace(/</g,'&lt;').replace(/>/g,'&gt;');
}

document.getElementById('btn-next').addEventListener('click', stepNext);
document.getElementById('btn-prev').addEventListener('click', stepPrev);
document.getElementById('btn-all').addEventListener('click', showAll);
document.getElementById('btn-reset').addEventListener('click', () => {
  loadFormula(document.getElementById('formula-select').value);
});
document.getElementById('formula-select').addEventListener('change', function() {
  loadFormula(this.value);
});

loadFormula(0);

<p class="hint">
  Resolution derives new clauses by canceling complementary literals. From clause
      <i>(A&nbsp;∨&nbsp;x)</i> and <i>(B&nbsp;∨&nbsp;¬x)</i> you derive the resolvent
      <i>(A&nbsp;∨&nbsp;B)</i>. A <b>refutation</b> derives the empty clause ⊥,
      proving the formula is unsatisfiable. Step through the proof to see how length grows.
</p>
<div class="controls">
  <label for="formula-select">Formula:</label>
  <select id="formula-select">
    <option value="0">PHP(2,1) — 2 pigeons, 1 hole (4 steps)</option>
    <option value="1">PHP(3,2) — 3 pigeons, 2 holes (12 steps)</option>
    <option value="2">2-CNF clash — all four (x,y) combinations (6 steps)</option>
  </select>
</div>
<div class="proof-area">
  <div class="clause-list" id="clause-list"></div>
</div>
<div class="step-info" id="step-info">Press "Next Step" to begin the refutation.</div>
<div class="btns">
  <button id="btn-prev" type="button" class="ghost" disabled>← Prev</button>
  <button id="btn-next" type="button">Next Step →</button>
  <button id="btn-all" type="button" class="ghost">Show All</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="stats" id="stats"></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 .6rem; line-height: 1.45; }
.controls { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; flex-wrap: wrap; }
label { font-weight: 600; font-size: .88rem; }
select { font-size: .88rem; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px;
         background: #f5f7fa; cursor: pointer; }
.proof-area { border: 1px solid #cdd9e3; border-radius: 8px; background: #f8fafc;
              padding: .5rem .7rem; min-height: 120px; max-height: 220px; overflow-y: auto;
              margin-bottom: .5rem; }
.clause-list { display: flex; flex-direction: column; gap: 3px; }
.clause-row { display: flex; align-items: baseline; gap: .5rem; font-size: .85rem;
              padding: 2px 0; }
.clause-row.axiom  { color: #1d3557; }
.clause-row.derived { color: #0a7d33; }
.clause-row.empty-clause { color: #c92f3c; font-weight: 700; }
.clause-row.new { animation: fadeIn .3s ease; }
@keyframes fadeIn { from { opacity: 0; transform: translateY(-4px); } to { opacity: 1; } }
.row-num { color: #888; font-size: .75rem; min-width: 24px; text-align: right; flex-shrink: 0; }
.clause-text { font-family: ui-monospace, monospace; }
.justification { color: #777; font-size: .75rem; font-style: italic; }
.step-info { font-size: .9rem; font-weight: 600; margin: .4rem 0; min-height: 1.4em;
             color: #1d3557; }
.btns { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .4rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .8rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .4; cursor: not-allowed; }
.stats { font-size: .82rem; color: #555; min-height: 1.2em; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Resolution proof demo for three unsatisfiable propositional formulas.
//
// Literal encoding: positive literal = string like ’p11’; negative = ’¬p11’.
// Resolution rule: from (A ∨ x) and (B ∨ ¬x) derive the resolvent (A ∨ B).
// A resolution REFUTATION is a sequence of clauses, each an axiom or resolvent
    // of two earlier clauses, ending with the empty clause ⊥.
//
// Formula 0: PHP(2,1) — Pigeonhole principle: 2 pigeons, 1 hole.
//   Variables p11, p21. Axioms: (p11), (p21), (¬p11 ∨ ¬p21).
//   Resolution refutation in 2 derived steps (4 total).
//
// Formula 1: PHP(3,2) — Pigeonhole principle: 3 pigeons, 2 holes.
//   Variables pij. Axioms: pigeon-must-go-somewhere (A), no-sharing (B).
//   Resolution refutation in 12 derived steps (21 total).
//
// Formula 2: 2-CNF full clash on two variables x, y.
//   Clauses: (x ∨ y), (x ∨ ¬y), (¬x ∨ y), (¬x ∨ ¬y).
//   Clearly unsat (covers all 4 assignments). Refutation in 3 derived steps (7 total).
//   Shows how a Frege-style system (or extended resolution) can be shorter.

function negLit(l) { return l.startsWith('¬') ? l.slice(1) : '¬' + l; }

// Verify that child is a valid resolvent of c1 and c2
function isValidResolvent(c1, c2, child) {
  for (const l of c1) {
    const nl = negLit(l);
    if (c2.includes(nl)) {
      const res = [...c1.filter(x => x !== l), ...c2.filter(x => x !== nl)];
      const seen = new Set();
      const uniq = res.filter(x => { if (seen.has(x)) return false; seen.add(x); return true; });
      const cs = new Set(child); const es = new Set(uniq);
      if (cs.size === es.size && [...cs].every(x => es.has(x))) return true;
    }
  }
  return false;
}

function buildProof(formulaIdx) {
  const steps = [];
  function addAxiom(lits, just) {
    steps.push({ lits, type: 'axiom', just });
    return steps.length - 1;
  }
  function addStep(lits, just, p1, p2) {
    if (!isValidResolvent(steps[p1].lits, steps[p2].lits, lits)) {
      console.error(fmt('Invalid resolvent at step %length%%v%', { length: steps.length, v: 1 }),
        steps[p1].lits, '+', steps[p2].lits, '->', lits);
    }
    steps.push({ lits, type: lits.length === 0 ? 'empty-clause' : 'derived', just, parents: [p1, p2] });
    return steps.length - 1;
  }

  if (formulaIdx === 0) {
    // PHP(2,1): 2 pigeons, 1 hole
    // A-clauses: pigeon i must go in hole 1
    const a1 = addAxiom(['p11'], 'Axiom: pigeon 1 must go in hole 1');
    const a2 = addAxiom(['p21'], 'Axiom: pigeon 2 must go in hole 1');
    // B-clause: hole 1 can hold at most one pigeon
    const b  = addAxiom(['¬p11', '¬p21'], 'Axiom: hole 1 holds at most 1 pigeon');
    // Resolution refutation:
    const s1 = addStep(['¬p21'], 'Res(1, 3) on p11 — pigeon 2 out of hole 1', a1, b);
    addStep([], 'Res(2, 4) on p21 → ⊥ contradiction', a2, s1);

  } else if (formulaIdx === 1) {
    // PHP(3,2): 3 pigeons, 2 holes
    // A-axioms: 0=(p11∨p12), 1=(p21∨p22), 2=(p31∨p32)
    addAxiom(['p11', 'p12'], 'Axiom: pigeon 1 in hole 1 or 2');
    addAxiom(['p21', 'p22'], 'Axiom: pigeon 2 in hole 1 or 2');
    addAxiom(['p31', 'p32'], 'Axiom: pigeon 3 in hole 1 or 2');
    // B-axioms hole 1: 3=(¬p11∨¬p21), 4=(¬p11∨¬p31), 5=(¬p21∨¬p31)
    addAxiom(['¬p11', '¬p21'], 'Axiom: hole 1 holds at most 1 (pigeons 1,2)');
    addAxiom(['¬p11', '¬p31'], 'Axiom: hole 1 holds at most 1 (pigeons 1,3)');
    addAxiom(['¬p21', '¬p31'], 'Axiom: hole 1 holds at most 1 (pigeons 2,3)');
    // B-axioms hole 2: 6=(¬p12∨¬p22), 7=(¬p12∨¬p32), 8=(¬p22∨¬p32)
    addAxiom(['¬p12', '¬p22'], 'Axiom: hole 2 holds at most 1 (pigeons 1,2)');
    addAxiom(['¬p12', '¬p32'], 'Axiom: hole 2 holds at most 1 (pigeons 1,3)');
    addAxiom(['¬p22', '¬p32'], 'Axiom: hole 2 holds at most 1 (pigeons 2,3)');
    // 12-step resolution refutation (all verified):
    const s1  = addStep(['p12', '¬p21'], 'Res(1,4) on p11', 0, 3);
    const s2  = addStep(['p12', 'p22'],  'Res(s1,2) on p21', s1, 1);
    const s3  = addStep(['p12', '¬p31'], 'Res(1,5) on p11', 0, 4);
    const s4  = addStep(['p12', 'p32'],  'Res(s3,3) on p31', s3, 2);
    const s5  = addStep(['p22', '¬p32'], 'Res(s2,8) on p12', s2, 7);
    const s6  = addStep(['p22', 'p31'],  'Res(s5,3) on p32', s5, 2);
    const s7  = addStep(['p22', '¬p21'], 'Res(s6,6) on p31', s6, 5);
    const s8  = addStep(['p22'],          'Res(s7,2) on p21', s7, 1);
    const s9  = addStep(['¬p32'],         'Res(s8,9) on p22', s8, 8);
    const s10 = addStep(['p12'],          'Res(s4,s9) on p32', s4, s9);
    const s11 = addStep(['¬p12'],         'Res(s8,7) on p22', s8, 6);
    addStep([], 'Res(s10,s11) on p12 → ⊥', s10, s11);

  } else {
    // 2-CNF full clash: (x∨y) ∧ (x∨¬y) ∧ (¬x∨y) ∧ (¬x∨¬y)
    // Unsatisfiable: every truth assignment falsifies at least one clause.
    addAxiom(['x', 'y'],   'Axiom: (x ∨ y)');
    addAxiom(['x', '¬y'],  'Axiom: (x ∨ ¬y)');
    addAxiom(['¬x', 'y'],  'Axiom: (¬x ∨ y)');
    addAxiom(['¬x', '¬y'], 'Axiom: (¬x ∨ ¬y)');
    // Refutation in 3 steps:
    // (x∨y) + (x∨¬y) resolve on y -> (x)
    const s1 = addStep(['x'],  'Res(1,2) on y — x must be true', 0, 1);
    // (¬x∨y) + (¬x∨¬y) resolve on y -> (¬x)
    const s2 = addStep(['¬x'], 'Res(3,4) on y — x must be false', 2, 3);
    // (x) + (¬x) -> ⊥
    addStep([], 'Res(s1,s2) on x → ⊥ (x can’t be both true and false)', s1, s2);
  }
  return steps;
}

// ── State ────────────────────────────────────────────────────────────────────
let allSteps = [];
let shownCount = 0;

function loadFormula(idx) {
  allSteps = buildProof(Number(idx));
  shownCount = 0;
  renderList();
  updateInfo('Press "Next Step" to begin the refutation.');
  updateStats();
  updateButtons();
}

function fmtLits(lits) {
  if (lits.length === 0) return '⊥';
  return '(' + lits.join(' ∨ ') + ')';
}

function renderList() {
  const list = document.getElementById('clause-list');
  list.innerHTML = '';
  for (let i = 0; i < shownCount; i++) {
    const s = allSteps[i];
    const row = document.createElement('div');
    row.className = 'clause-row ' + s.type + (i === shownCount - 1 ? ' new' : '');
    row.innerHTML =
      '<span class="row-num">' + (i + 1) + '.</span>' +
      '<span class="clause-text">' + escHtml(fmtLits(s.lits)) + '</span>' +
      '<span class="justification">' + escHtml(s.just) + '</span>';
    list.appendChild(row);
  }
  document.querySelector('.proof-area').scrollTop = 9999;
}

function updateInfo(msg) {
  document.getElementById('step-info').textContent = msg;
}

function updateStats() {
  const axiomCount = allSteps.filter(s => s.type === 'axiom').length;
  const derivedShown = Math.max(0, shownCount - axiomCount);
  document.getElementById('stats').textContent =
    fmt('Axioms: %axiomCount% | Derived steps shown: %derivedShown% | Total proof length: %length% steps', { axiomCount: axiomCount, derivedShown: derivedShown, length: allSteps.length });
}

function updateButtons() {
  document.getElementById('btn-prev').disabled = shownCount <= 0;
  document.getElementById('btn-next').disabled = shownCount >= allSteps.length;
  document.getElementById('btn-all').disabled = shownCount >= allSteps.length;
}

function stepNext() {
  if (shownCount >= allSteps.length) return;
  shownCount++;
  const s = allSteps[shownCount - 1];
  renderList();
  if (s.type === 'axiom') {
    updateInfo(fmt('Axiom %shownCount%: %fmtLits%', { shownCount: shownCount, fmtLits: fmtLits(s.lits) }));
  } else if (s.type === 'empty-clause') {
    updateInfo(fmt('⊥ derived — refutation complete in %length% total steps!', { length: allSteps.length }));
  } else {
    updateInfo(fmt('Step %shownCount%: %just% → %fmtLits%', { shownCount: shownCount, just: s.just, fmtLits: fmtLits(s.lits) }));
  }
  updateStats();
  updateButtons();
}

function stepPrev() {
  if (shownCount <= 0) return;
  shownCount--;
  renderList();
  updateInfo(shownCount === 0
    ? 'Press "Next Step" to begin the refutation.'
    : fmt('Step %shownCount%: %fmtLits%', { shownCount: shownCount, fmtLits: fmtLits(allSteps[shownCount - 1].lits) }));
  updateStats();
  updateButtons();
}

function showAll() {
  shownCount = allSteps.length;
  renderList();
  updateInfo(fmt('Full proof shown — %length% total steps, ending in ⊥.', { length: allSteps.length }));
  updateStats();
  updateButtons();
}

function escHtml(s) {
  return s.replace(/&/g,'&amp;').replace(/</g,'&lt;').replace(/>/g,'&gt;');
}

document.getElementById('btn-next').addEventListener('click', stepNext);
document.getElementById('btn-prev').addEventListener('click', stepPrev);
document.getElementById('btn-all').addEventListener('click', showAll);
document.getElementById('btn-reset').addEventListener('click', () => {
  loadFormula(document.getElementById('formula-select').value);
});
document.getElementById('formula-select').addEventListener('change', function() {
  loadFormula(this.value);
});

loadFormula(0);

Result

Console

Watch how the number of steps (lines in the proof) grows as the formula changes. PHP(2,1) needs 5 steps, PHP(3,2) needs 21 — and for PHP(n+1, n) in general, resolution needs at least $2^{\Omega(n)}$ steps (proven by Haken, 1985). The 2-CNF clash formula collapses to just 7 steps because it has a small proof in resolution too — but for harder formulas, no shortcut exists inside weak systems.

The Real Complexity

Proof complexity ranks proof systems by the lengths they require:

Resolution is the weakest widely studied system. It operates on clauses (disjunctions of literals) and derives new clauses by the single resolution rule. Armin Haken (1985) proved that the pigeonhole principle — "you can't fit $n+1$ pigeons into $n$ holes without sharing" — requires exponentially many resolution steps. This was the field's first superpolynomial lower bound.
Ben-Sasson and Wigderson (2001) gave an elegant reformulation: proof length in resolution is controlled by clause space and clause width. Their Width–Size theorem connects these three measures and gives a clean recipe for proving lower bounds.
Frege systems (sequent calculus, natural deduction) are far more powerful: they can manipulate arbitrary formulas, not just clauses. No superpolynomial lower bound is known for any Frege system. Proving one would separate NP from co-NP.
Extended Frege adds the power to introduce abbreviations (extension variables). It is conjectured to be polynomially equivalent to circuit-based proof systems. Its complexity is entirely open.
The Cook–Reckhow theorem (1979): a propositional proof system $P$ can always produce short (polynomial-length) proofs of all tautologies if and only if the language of tautologies is in NP — which happens exactly when NP = co-NP. So finding a proof system with short proofs for everything would resolve a major open problem.

The landscape: resolution is weak and well understood; Frege is strong and mysterious; everything in between is an active frontier.

Where It Matters

Proof complexity is not just abstract logic — it shapes the tools that power modern computer science:

SAT solvers and CDCL: modern SAT solvers use Conflict-Driven Clause Learning, which implicitly builds resolution proofs as they search. The strength of CDCL is captured by a fragment of resolution called pool resolution, and understanding proof length explains why some instances are hard for solvers.
Automated theorem proving: every theorem prover must choose a proof calculus. Proof complexity tells us which calculi can be efficiently complete and which will inevitably bloat.
Cryptography: some proof-of-work schemes require hard instances where short proofs of satisfiability exist but are hard to find. Proof complexity provides the theoretical grounding.
Circuit lower bounds: there is a deep connection between proof complexity and circuit complexity. Proving lower bounds for Frege systems would likely require breakthroughs in understanding the power of $\mathsf{TC}^0$ circuits.
The NP vs co-NP question: as Cook and Reckhow showed, a proof system with polynomial-size proofs for all tautologies would collapse NP and co-NP — one of the most important open questions alongside P vs NP.

Conclusion

Proof complexity teaches a sobering lesson: correctness and certifiability are different things. A formula can be unsatisfiable — provably, absolutely false — yet every proof of that fact in a given system must be exponentially long. Resolution is provably weak; Frege systems remain a mystery after decades of effort.

The question of whether there is a proof system that is always efficient is equivalent to NP = co-NP, which is itself implied by P = NP. So the shortest path to the P vs NP Millennium Prize may run straight through proof complexity — through the unavoidable length of proofs we write every day.

Comments

Loading comments...

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

Cookies & privacy

When the proof itself is the bottleneck