The Resolution Proof Method

Logic programming and automated reasoning systems heavily rely on a proof technique called Resolution. Unlike natural deduction, which can feel like guesswork, resolution is a refutation procedure -- it tries to prove a formula is unsatisfiable.

The Core Concept

Resolution works on formulas in Clausal Form (a conjunction of disjunctions). The fundamental rule is similar to the "cut" rule in logic. If we have two clauses that contain complementary literals (e.g., $p$ and $\neg p$), we can "resolve" them to create a new clause.

$$ \\frac{\{p, r\}, \\{\\neg p, q\}}{\\{r, q\}} $$

If we can derive the empty clause (denoted as $\square$), we have found a contradiction, proving that the original set of premises is unsatisfiable.

Unification: Making Terms Match

In propositional logic, matching $P$ and $\neg P$ is easy. In First-Order Logic, we deal with variables and functions, like $P(f(x))$ and $\neg P(y)$. To resolve these, we need Unification.

Unification is the process of finding a substitution $\theta$ that makes two expressions identical. For example, to unify $P(x, f(y))$ and $P(a, z)$:

• We substitute $x$ with $a$ (substitution $\{x/a\}$).
• We substitute $z$ with $f(y)$ (substitution $\{z/f(y)}\).

This results in the unified term $P(a, f(y))$.

The Occurs Check

A famous pitfall in unification is the "occurs check." If we try to unify $x$ with $f(x)$, a naive algorithm might try to substitute $x$ into the function infinitely, creating $f(f(f(...)))$. Standard unification requires checking if the variable occurs inside the term it is being unified with. Interestingly, essentially all Prolog implementations omit this check for efficiency, even though it technically destroys soundness.