Resolution refutation: proving theorems by contradiction

One rule to prove them all

Everything in Module 1 — modus ponens, modus tollens, unification — built toward a single, mechanical procedure that a computer can run *without* domain knowledge. That procedure is resolution refutation, and its appeal is that it needs exactly one inference rule. Combined with clause-form conversion, resolution is refutation-complete for predicate calculus: if a set of clauses is unsatisfiable, resolution can always find the contradiction. This is the formal foundation under Prolog and under every expert-system shell — a *weak method* in the technical sense (general, not domain-specific).

The strategy: prove by contradiction

Resolution does not derive the goal forward. Instead it assumes the goal is false and shows that this assumption is *inconsistent* with what we already know. If "the axioms plus the negated goal" lead to a contradiction, then the goal must follow from the axioms. The contradiction has a precise syntactic form: the empty clause $\square$ — a clause with no literals, which can never be satisfied.

The five steps

1. Put all premises/axioms in clause form (conjunctive normal form): a conjunction of disjunctions of literals, with all quantifiers eliminated.
2. Negate the theorem to be proved and convert *it* to clause form too; add it to the clause set.
3. Resolve repeatedly. When two clauses contain complementary literals ($a$ in one, $\lnot a$ in the other), the resolvent is the disjunction of all *other* literals from both clauses. With variables, the literals must first be made identical by their most general unifier (mgu), and that substitution is applied to the whole resolvent.
4. Derive the empty clause $\square$ — a contradiction.
5. Read off the answer. The unification substitutions accumulated along the way are the variable bindings under which the original theorem is true (answer extraction).

Worked example — prove $Q$ from $P \to Q$ and $P$

First, clause form. The rule $P \to Q$ becomes the clause $\{\lnot P, Q\}$ (because $P\to Q \equiv \lnot P \lor Q$). The fact $P$ is the unit clause $\{P\}$. We want to prove $Q$, so we negate it: add $\{\lnot Q\}$.

Now resolve, using set of support (every step must involve the negated goal or one of its descendants — a complete, focused strategy):

- Resolve $\{\lnot Q\}$ with $\{\lnot P, Q\}$. The complementary pair is $Q / \lnot Q$; the resolvent keeps the rest: $\{\lnot P\}$. - Resolve $\{\lnot P\}$ with $\{P\}$. The pair is $P / \lnot P$; nothing remains: the resolvent is $\square$, the empty clause.

$\square$ means contradiction, so the negated goal was impossible — therefore $Q$ is proved. Notice this is exactly *modus ponens* run backwards through cancellation: $Q$ and $\lnot Q$ cancel, $P$ and $\lnot P$ cancel, and the cancellation to nothing is the proof.

Skolemization (why $\exists$ disappears)

Resolution works syntactically on terms, so existential quantifiers must go. Skolemization replaces an existentially quantified variable with a witness. A bare $\exists Y\,foo(Y)$ becomes a Skolem constant $foo(k)$. But inside a universal — $\forall X\,\exists Y\,mother(X,Y)$ — the $Y$ *depends on* $X$, so it becomes a Skolem function: $\forall X\,mother(X, m(X))$ (every $X$ has their own mother $m(X)$). Skolem functions also carry the answer in answer extraction: proving "John has a grandparent" yields the term $pa(pa(john))$.

Search strategies (resolution still needs control)

Resolution is one rule, but *which* pairs to resolve is a search problem with combinatorial blow-up. Four strategies tame it:

- Breadth-first — all level-$n$ resolvents before level $n{+}1$. Complete, but exponential. - Set of support — every step uses the negated goal or a descendant of it. Complete when the premises alone are consistent, and far more focused (used in the worked example). - Unit preference — prefer resolving with single-literal (unit) clauses, which shrinks clauses fastest. A useful efficiency heuristic; incomplete on its own. - Linear input form — always resolve the newest clause against an *original* axiom. Complete for Horn-clause databases (this is exactly what makes Prolog efficient) but not for general clauses.

Two housekeeping simplifications keep the clause space small: tautology elimination (discard any clause containing both $p$ and $\lnot p$ — it can never help) and subsumption (discard a clause already implied by a more general one). Both preserve completeness while cutting work — the formal analog of pruning a search tree.