Resolution and Inference

Resolution is a single inference rule that, applied repeatedly, is complete for first-order logic. The trick: convert everything to CNF clauses; then resolution does the rest.

Resolution rule

From clauses $C_1 = A \vee L$ and $C_2 = B \vee \neg L$, infer the resolvent $C_1 \cup C_2 \setminus \{L, \neg L\}$ — that is, $A \vee B$. The literal $L$ "resolves" away.

In first-order logic, unification figures out variable substitutions to make $L$ and $\neg L$ match up. The resulting resolvent has the variables substituted accordingly.

Refutation completeness

To prove $\alpha \models \beta$:

1. Convert $\alpha \wedge \neg \beta$ to CNF. 2. Apply resolution until you derive the empty clause $\Box$ (a contradiction) or no new clauses can be derived. 3. If empty clause is derived, $\alpha \wedge \neg \beta$ is unsatisfiable, so $\alpha \models \beta$.

Robinson (1965) showed this is complete for first-order logic — anything entailed is provable by resolution.

Skolemization

To get FOL formulas into CNF, you need to eliminate existential quantifiers. Replace $\exists x \, P(x)$ with $P(\text{sk}_1)$ for a fresh constant. If existentials are inside a universal, use a Skolem function: $\forall y \, \exists x \, P(x, y) \Rightarrow \forall y \, P(\text{sk}(y), y)$.

Skolemization preserves satisfiability (not equivalence — that's why this is fine for proofs but you can't just pretend a Skolem function "is" the existential).

Unification

To resolve $P(x)$ with $\neg P(\text{Socrates})$, find a substitution $\theta$ such that $P(x)\theta = P(\text{Socrates})\theta$. Here $\theta = \{x / \text{Socrates}\}$. The most general unifier (MGU) is the substitution that commits to the least — exactly what you want for general theorem proving.

Strategies

Naive resolution generates astronomically many clauses. Practical theorem provers use:

• Set of support: only resolve clauses derived from the (negated) goal. Focuses the search.
• Linear resolution: each new resolvent uses the most recently derived clause.
• Unit preference: resolve with unit clauses (single literals) when possible — they always produce shorter resolvents.
• Subsumption: discard a clause if a strictly shorter clause already implies it.

Modern theorem provers

Vampire, E, Prover9 implement sophisticated variants of resolution and have proved nontrivial open problems in mathematics. But for everyday AI use, decidable subsets of FOL (Datalog, description logic, SAT/SMT) get you most of the value with predictable termination.