First-Order Resolution

This builds on Inference in First-Order Logic, which lifted propositional inference to first order through unification and built the forward- and backward-chaining algorithms for Horn knowledge bases. Here we drop the Horn restriction and give a single complete rule for all of first-order logic.

Resolution

Chaining is complete only for definite clauses — Horn knowledge bases. General first-order sentences, with disjunctive conclusions and negations, need a single sound and complete rule: resolution.¹ It proves $KB\models \alpha$ by refutation — showing $KB\wedge \neg \alpha$ unsatisfiable — and it operates on sentences in conjunctive normal form.

Conversion to CNF

Every first-order sentence has an inferentially equivalent conjunctive normal form (CNF): a conjunction of clauses, each a disjunction of literals, with variables understood as universally quantified. The rule $(9.3)$ becomes the single clause

The conversion is mechanical but has one first-order-specific step. Consider

We eliminate implications ($\alpha ⟹\beta$ becomes $\neg \alpha \vee \beta$); push negations inward, using $\neg \forall xp\equiv \exists x\neg p$ and $\neg \exists xp\equiv \forall x\neg p$; and standardize apart any reused quantifier variables. The remaining step has no propositional analogue.

Naively replacing the two existentials with constants $A$ and $B$ would assert that everyone fails to love one particular animal $A$ or is loved by one particular entity $B$ — the wrong meaning. Because the object depends on $x$, the Skolem entity must too, giving Skolem functions $F(x)$ and $G(x)$:

Now every remaining variable is universal, so we drop the quantifiers, distribute $\vee$ over $\wedge$, and read off the clauses. Skolemization is the general form of the existential-instantiation trick from the start of the lesson; the Skolemized sentence is satisfiable exactly when the original is, which is all refutation needs.

Run all six stages on that sentence in full, so no step is left implicit. The starting point is

1. Eliminate implications. Rewrite each $\alpha ⟹\beta$ as $\neg \alpha \vee \beta$, both the outer one and the inner one:$$\forall x\neg [\forall y\neg Animal(y)\vee Loves(x,y)]\vee [\exists yLoves(y,x)].$$
2. Move negation inward. Push the leading $\neg$ through the universal, turning $\neg \forall y$ into $\exists y$ and negating the disjunction under it with De Morgan, so $\neg (\neg Animal(y)\vee Loves(x,y))$ becomes $Animal(y)\wedge \neg Loves(x,y)$:$$\forall x[\exists yAnimal(y)\wedge \neg Loves(x,y)]\vee [\exists yLoves(y,x)].$$
3. Standardize apart. The two $\exists y$ quantifiers bind unrelated variables reusing the name $y$; rename the second to $z$ so no later step confuses them:$$\forall x[\exists yAnimal(y)\wedge \neg Loves(x,y)]\vee [\exists zLoves(z,x)].$$
4. Skolemize. Both existentials lie inside $\forall x$, so the witnesses depend on $x$. Replace $y$ by the Skolem function $F(x)$ and $z$ by $G(x)$, and drop the existentials:$$\forall x[Animal(F(x))\wedge \neg Loves(x,F(x))]\vee Loves(G(x),x).$$
5. Drop universal quantifiers. Only $\forall x$ remains, and every free variable is now understood as universally quantified, so erase it:$$[Animal(F(x))\wedge \neg Loves(x,F(x))]\vee Loves(G(x),x).$$
6. Distribute $\vee$ over $\wedge$. The final form is a conjunction of clauses. Distributing the trailing disjunct across the conjunction splits the sentence into two clauses:$$[Animal(F(x))\vee Loves(G(x),x)]\wedge [\neg Loves(x,F(x))\vee Loves(G(x),x)].$$

Those two clauses are the input resolution will use later. Nothing in the sequence changed the sentence's satisfiability, and only stage 4 has no propositional counterpart.

The resolution rule

The first-order resolution rule is the lifted version of propositional resolution. Two clauses standardized apart can be resolved if one has a literal that unifies with the negation of a literal in the other; the resolvent is the union of the remaining literals with the unifier applied.

For instance, $[Animal(F(x))\vee Loves(G(x),x)]$ and $[\neg Loves(u,v)\vee \neg Kills(u,v)]$ resolve on the complementary $Loves(G(x),x)$ and $\neg Loves(u,v)$ under $\theta =\{u/G(x),v/x\}$, producing $[Animal(F(x))\vee \neg Kills(G(x),x)]$. Binary resolution alone is not quite complete; it must be paired with factoring, which collapses two literals in a clause to one when they are unifiable. The two together are complete.

Refutation

To prove $KB\models \alpha$, add $\neg \alpha$ to the knowledge base, convert everything to clauses, and resolve until the empty clause — a disjunction of no literals, denoting a contradiction — appears. On the crime example, negating the goal to $\neg Criminal(West)$ and resolving against the clause forms of $(9.3)$–$(9.10)$ produces a proof with a characteristic shape: a single spine, the goal clause resolving against one knowledge-base clause at a time until the empty clause drops out.

On Horn knowledge bases the clauses along the spine correspond exactly to the successive goals of backward chaining: backward chaining is resolution with a fixed strategy for choosing the next step. General knowledge bases give bushier proofs.

Curiosity killed the cat, in full

The Curiosity killed the cat puzzle is the standard example of a proof that is not a single spine. In English: everyone who loves all animals is loved by someone; anyone who kills an animal is loved by no one; Jack loves all animals; either Jack or Curiosity killed the cat, who is named Tuna; and Tuna is a cat while all cats are animals. Does Curiosity kill Tuna? Converting every sentence to clauses gives the knowledge base (variables universal, $F$ and $G$ the Skolem functions from the CNF trace above):²

Clauses A and B come from loves all animals is loved by someone; C from kills an animal, loved by no one; and to refute the query we add its negation, $\neg Kills(Curiosity,Tuna)$. Now resolve, tracking each resolvent and the unifier that produced it.

1. Resolve E with the negated goal on $Kills(Curiosity,Tuna)$, unifier $\{\}$: the two $Curiosity$ literals are already ground and complementary, leaving $Kills(Jack,Tuna)$.
2. Resolve that with C on $Kills(x,y)$, unifier $\{x/Jack,y/Tuna\}$, giving $\neg Animal(Tuna)\vee \neg Loves(z,Jack)$.
3. Resolve with D $=Animal(Tuna)$, unifier $\{\}$, discharging the first disjunct and leaving $\neg Loves(z,Jack)$: no one loves Jack.
4. Resolve with B on $Loves(G(x),x)$ against $\neg Loves(z,Jack)$, unifier $\{z/G(Jack),x/Jack\}$, giving $\neg Loves(Jack,F(Jack))$.
5. Resolve with F $=Loves(Jack,w)$, unifier $\{w/F(Jack)\}$: the two $Loves(Jack,\cdot )$ literals are complementary, and the resolvent is the empty clause.

The empty clause closes the proof, so $KB\models Kills(Curiosity,Tuna)$. The paraphrase reads as ordinary deduction: if Curiosity did not kill Tuna, Jack did (step 1); Tuna is an animal, so whoever killed it is loved by no one, in particular Jack (steps 2–3); but Jack loves all animals, so someone loves Jack (steps 4–5) — a contradiction. Step 4 uses clause B, which skolemization produced, and the general accounting also needs factoring; the version above threads a single lineage for readability.

One subtlety: for existential queries like who killed the cat? resolution can return a nonconstructive proof, deriving $\exists wKills(w,Tuna)$ without committing to a single $w$. Tracking an answer literal through the proof recovers the actual binding.

Completeness

Resolution is refutation-complete: if a set of clauses is unsatisfiable, a finite number of resolution steps derives the empty clause.³ The proof threads three results. Any unsatisfiable clause set has an unsatisfiable finite set of ground instances (Herbrand's theorem); propositional resolution is complete on those ground clauses (the ground resolution theorem); and a lifting lemma shows every ground resolution proof is the shadow of a first-order one, obtained by instantiating the MGU. So the empty clause reachable at the ground level is reachable with the original first-order clauses. Instantiating variables only as far as a proof requires, rather than exhaustively as propositionalization did, is resolution's advantage.

This refutation-completeness is the first-order side of a deep result. In 1930 Gödel proved that first-order logic has a complete proof procedure — every valid sentence is provable — and a refutation-complete resolution system is one way to realize it.

The result is not a promise of decidability — completeness says every entailment has a proof, while semidecidability says we cannot always tell when one is absent. And Gödel's later incompleteness theorem draws the boundary: extend the language with arithmetic and induction, and there are true sentences no proof system can reach. The completeness that resolution enjoys is a property of pure first-order logic, before that extension.

Resolution strategies

Refutation-completeness guarantees a proof exists; it says nothing about how long the search for it takes. Applying resolution to every pair of clauses generates a combinatorial flood of resolvents, most of them useless. A strategy is a rule restricting which pairs to resolve, chosen so the search reaches the empty clause sooner while keeping completeness.⁴

Two more devices prune rather than direct. Subsumption discards any clause already subsumed by one in the base — if $P(x)$ is known, the more specific $P(A)$ carries no new information and can be deleted, keeping the clause set free of redundancy. And clauses can be simplified by removing tautologies and duplicated literals before they ever enter the pool.

Handling equality

Resolution as stated treats $=$ as one more predicate, which is not enough: from $A=B$ and $P(A)$ it will not derive $P(B)$ without help, because the two $A$ terms never meet a complementary literal to resolve on. One remedy is to add the axioms of equality — reflexivity, symmetry, transitivity, and a substitution axiom for every function and predicate — but these generate large numbers of resolvents. The alternatives build equality reasoning into the inference rule.⁵

Paramodulation is the more general rule: it resolves on an equation without requiring it to be a separate unit clause, so equality reasoning interleaves with the rest of the proof. Resolution with paramodulation is refutation-complete for first-order logic with equality, and it is the equality machinery inside modern provers.

Modern automated theorem provers

The resolution and unification machinery in this lesson still runs inside the automated reasoning tools used today, though the winning provers refine it well past binary resolution. The dominant calculus is superposition, an ordered combination of resolution and paramodulation that uses term orderings to restrict which inferences are allowed. E, described by Stephan Schulz (2002, in the Journal of the AI Communications), and Vampire, described by Laura Kovács and Andrei Voronkov (2013, in Computer Aided Verification, CAV), are two saturation-based superposition provers built on this calculus; both take a first-order problem, saturate the clause set under the inference rules with the redundancy elimination and indexing sketched above, and search for the empty clause. These systems are compared each year at CASC, the CADE ATP System Competition, organized by Geoff Sutcliffe on the TPTP problem library.^byb-provers

A second line handles logic with background theories. SMT solvers — satisfiability modulo theories — pair a propositional SAT core with dedicated decision procedures for theories like linear arithmetic, arrays, and bit-vectors, so the Boolean search delegates theory-specific facts to a specialist rather than encoding them as clauses. Z3, described by Leonardo de Moura and Nikolaj Bjørner (2008, in Tools and Algorithms for the Construction and Analysis of Systems, TACAS), is one such solver, used widely in program verification and symbolic execution. The division of labor echoes this lesson's split between a general search procedure and specialized handling of equality: SMT generalizes that idea to a whole catalog of theories.

The heritage runs back through Prolog. The answer-set programming family and modern Datalog engines descend from the logic-programming and resolution tradition, with declarative languages whose execution is inference over Horn-like rules. What began as a proof procedure for pure first-order logic became a set of engines that verify programs, solve constraints, and answer database queries.

Where inference leads

Unification underlies everything here. It turns universal instantiation from an infinite enumeration into a targeted match; it lifts modus ponens into generalized modus ponens, which drives forward and backward chaining and underwrites Prolog; and lifted into the resolution rule, it makes a single complete proof procedure possible. The rest is strategy — data-driven versus goal-driven, Horn-restricted chaining versus general refutation. What all of it computes is entailment: what follows, with certainty, from what is known. The next module turns that capability outward, using logical representation and inference to choose actions rather than merely deduce facts, in classical planning.