1.3 Resolution and theorem proving

Resolution Rule for Clause Derivation

Resolution is a single, powerful inference rule that lets you derive new clauses from existing ones. When combined with a proof-by-contradiction strategy, it becomes the backbone of automated theorem proving: you can mechanically determine whether a set of clauses is satisfiable, or whether a conclusion follows from given premises.

Applying the Resolution Rule

The resolution rule works on two parent clauses that contain complementary literals, meaning some literal $L$ appears in one clause and $\neg L$ appears in the other. The rule produces a new clause called the resolvent by combining all the remaining literals from both parents, dropping the complementary pair.

For example, given the clauses $\{P, Q\}$ and $\{\neg P, R\}$, the complementary literals are $P$ and $\neg P$. Resolving on $P$ yields the resolvent $\{Q, R\}$.

A few things to keep in mind:

• You resolve on exactly one complementary pair at a time. If two clauses share more than one complementary pair, you still pick just one per resolution step.
• The resolvent is a logical consequence of the parent clauses. If both parents are true under some interpretation, the resolvent must be true under that interpretation too.
• Duplicate literals in the resolvent are removed (since $\{P, P, Q\}$ is the same clause as $\{P, Q\}$).

Properties of the Resolution Rule

Each clause is a disjunction of literals (propositional variables or their negations), and a clause set represents the conjunction of those clauses. Resolution operates within this conjunctive normal form (CNF) framework.

• Soundness. Resolution preserves logical consequence. Any resolvent is entailed by its parent clauses, so you never derive something false from something true.
• Refutation completeness. If a set of clauses is unsatisfiable, resolution is guaranteed to derive the empty clause $\square$. This is a slightly different claim than "you can derive any entailed clause directly." Resolution is complete for refutation, which is exactly what theorem proving by contradiction needs.

Resolution Proofs for Satisfiability

Constructing Resolution Proofs

A resolution proof is a sequence of resolution steps aimed at deriving the empty clause $\square$, which is a clause with no literals. Since a clause is a disjunction, a clause with no disjuncts is trivially false. Deriving $\square$ means the clause set is unsatisfiable.

To prove that a conclusion $\varphi$ follows from premises $\Gamma$:

1. Convert all premises in $\Gamma$ to CNF.
2. Negate the conclusion: take $\neg \varphi$ and convert it to CNF as well.
3. Combine all resulting clauses into a single clause set.
4. Repeatedly apply the resolution rule to pairs of clauses, adding each resolvent to the set.
5. If you derive $\square$, the original set $\Gamma \cup \{\neg \varphi\}$ is unsatisfiable, which means $\Gamma \models \varphi$.

Resolution proofs are often drawn as a tree (or DAG) where each internal node is a resolvent and its two children are the parent clauses used to produce it. The root of the tree is $\square$.

Interpreting Resolution Proofs

• Empty clause derived. The clause set is unsatisfiable. If you added $\neg \varphi$ to your premises, this means the premises entail $\varphi$.
• No new clauses can be generated. Resolution has saturated the clause set without producing $\square$. The clause set is satisfiable, and the premises do not entail the negated conclusion. You can read off a satisfying assignment from the saturated set.

This gives resolution a decision-procedure character for propositional logic: it always terminates (the number of distinct clauses over a finite set of variables is finite) and gives a definitive yes-or-no answer.

Unification in Resolution

Role of Unification

Unification becomes relevant when you move beyond propositional logic into first-order logic, where clauses can contain variables, constants, and function symbols. In propositional resolution, checking for complementary literals is just a syntactic match. In first-order resolution, two literals might become complementary only after substituting appropriate terms for variables.

Unification is the process of finding a substitution $\theta$ (a mapping from variables to terms) that makes two expressions syntactically identical. For instance, $P(x, f(a))$ and $P(b, y)$ unify under $\theta = \{x \mapsto b,\; y \mapsto f(a)\}$.

Unification Algorithm

The standard unification algorithm takes two expressions as input and either returns a substitution or reports failure:

1. If both expressions are identical, return the empty substitution.
2. If one is a variable $x$ and the other is a term $t$ that does not contain $x$ (the occurs check), return $\{x \mapsto t\}$.
3. If both are compound expressions with the same top-level symbol, recursively unify their arguments, composing substitutions as you go.
4. Otherwise, fail.

The result, when it exists, is the most general unifier (MGU): the substitution that imposes the fewest constraints on variables. Any other unifier can be obtained by further instantiating the MGU.

Resolution-Based Theorem Proving Algorithms

Basic Steps

A resolution-based theorem prover automates the refutation procedure described above. The core algorithm:

1. Convert to CNF. Transform all input formulas (premises and the negated conclusion) into conjunctive normal form.
2. Initialize the clause set. Collect all resulting clauses.
3. Select a pair of clauses that contain complementary literals.
4. Resolve them to produce a resolvent.
5. Add the resolvent to the clause set (if it isn't already present).
6. Terminate if the empty clause $\square$ is derived (unsatisfiable) or if no new resolvents can be produced (satisfiable).

Efficiency and Optimizations

Naively resolving every possible pair of clauses leads to an explosion of redundant clauses. Several strategies keep the search manageable:

• Unit preference. Prioritize clauses with a single literal (unit clauses). Resolving with a unit clause always produces a resolvent shorter than the other parent, driving the proof toward $\square$ faster.
• Set of support. Only resolve clause pairs where at least one clause descends from the negated conclusion. This prevents aimless derivations among the premises alone.
• Subsumption. If clause $C_1$ is a subset of clause $C_2$ (every literal in $C_1$ appears in $C_2$), then $C_2$ is redundant and can be discarded. $C_1$ is strictly more informative.
• Tautology elimination. Discard any clause containing both $L$ and $\neg L$, since it's trivially true and contributes nothing to a refutation.
• Ordering strategies. Fix an ordering on literals and only resolve on the maximal literal in each clause. This restricts the number of possible resolution steps without sacrificing completeness (under appropriate conditions).

Resolution-based provers built on these ideas are used in formal verification, automated mathematics, and AI reasoning systems. The key takeaway for this course: resolution gives you a mechanical, complete method for propositional theorem proving, and the same architecture extends naturally to first-order logic once you add unification.