Resolution (Concept) in First-Order Logic — Beginner-Friendly Notes

1. What It Is

General resolution is a complete inference procedure for any FOL KB (not just Horn). Like propositional resolution but with unification and handling quantifiers via CNF with Skolemization.

Propositional resolution + unification + quantifier handling = FOL resolution.

2. Steps at a Glance (for exam you list them)

1. Convert sentences to CNF:

   • Eliminate $\Rightarrow, \Leftrightarrow$
   • Move $
     eg$inward (De Morgan +$
     eg \forall \equiv \exists
     eg$)
   • Standardise variables, Skolemize (remove $\exists$ by introducing Skolem constants/functions — e.g., $\exists x\ P(x)$ → $P(A)$ where $A$ is new)
   • Drop $\forall$, distribute $\lor$ over $\land$

2. Refutation: add $
   eg α$ to KB, convert to CNF.

3. Apply resolution: from $(C \lor P)$ and $(D \lor
   eg Q)$where$P$and$Q$**unify** with substitution$\theta = mgu(P,Q)$, infer$(C \lor D)\theta$.

4. If empty clause $□$ derived → $KB \models α$ proved.

3. Unification — Key New Idea

Unify = find substitution that makes two literals identical. MGU = most general unifier.

Example: $Likes(x, John)$ and $Likes(Mary, y)$ unify with $\theta = \{x/Mary, y/John\}$ → $Likes(Mary, John)$.

Failure: $Likes(x, John)$ and $Likes(x, Mary)$ never unify (John ≠ Mary).

4. Tiny Example

KB: $\forall x\ (Bird(x) \Rightarrow Flies(x))$, $Bird(Tweety)$; Query $Flies(Tweety)$:

• CNF: ${
  eg Bird(x) \lor Flies(x)}, {Bird(Tweety)}, {
  eg Flies(Tweety)}$ (negated query)
• Resolve $
  eg Bird(x) \lor Flies(x)$with$
  eg Flies(Tweety)$via${x/Tweety}$? Actually need$Flies(x)$with$
  eg Flies(Tweety)$→${x/Tweety}$→$
  eg Bird(Tweety)$
• Resolve $
  eg Bird(Tweety)$with$Bird(Tweety)$→$□$ → proved.

5. Why Important

Property	Value
Sound	Yes
Complete	Yes for FOL (refutation) — can prove any entailed α
Semi-decidable	If $KB \models α$, resolution will eventually find $□$; if not, may loop forever (FOL is undecidable)

6. Use in AI

• Automated theorem provers, Prolog's underlying engine can be seen as restricted resolution.
• Basis for reasoning in many KR systems (but Horn chaining is preferred for efficiency when possible).

7. One-Line Summary

First-order resolution converts KB and negated query to CNF via Skolemization, then repeatedly resolves complementary literals under MGU to derive $□$, providing sound and refutation-complete inference for full FOL at the cost of semi-decidability.

8. Quick Self-Check

1. What does Skolemization do?
2. Why does FOL resolution need unification but propositional does not?