Inference in First-Order Logic: Overview

Chapter 9 — Inference in First-Order Logic Book: Artificial Intelligence: A Modern Approach (Russell & Norvig, 4th ed) Pages: 291–330

The Core Challenge

In propositional logic, we enumerate models or derive clauses over a finite symbol set.

In FOL, the domain is potentially infinite — we cannot enumerate all objects. We need new inference machinery.

Three Approaches

Approach Idea Completeness
Propositionalization Ground out all variables → reduce to propositional Semi-complete
Lifting (generalized rules) Apply inference rules directly to FOL sentences using unification Complete
Resolution (FOL) Skolemize, convert to CNF, generalized resolution Refutation-complete

Universal Instantiation (UI)

For any sentence with universal quantifier and any ground term g:

∀v α
────────────────
SUBST({v/g}, α)

Example: - ∀x King(x) ∧ Greedy(x) → Evil(x) + King(John) + Greedy(John) - Apply UI with g=John: King(John) ∧ Greedy(John) → Evil(John) - Modus ponens: Evil(John)

UI can be applied to any ground term — including complex ones like Father(Father(John)).

Existential Instantiation (EI)

When ∃x α, introduce a Skolem constant — a new symbol not in the KB:

∃x α
────────────────
SUBST({x/k}, α)   where k is a new constant

Example: - ∃x Crown(x) ∧ OnHead(x, John) - Introduce C1 (Skolem constant) - Derive: Crown(C1) ∧ OnHead(C1, John)

EI is used once — the Skolem constant represents “whichever object satisfies the existential.”

Propositionalization

Idea: enumerate all ground substitutions of universally quantified variables → get a propositional KB → apply propositional inference.

Herbrand’s theorem (1930): if a FOL KB is unsatisfiable, a finite subset of the propositionalized KB is also unsatisfiable.

Procedure: 1. Apply UI to generate all ground instances of universally quantified sentences 2. Run propositional inference on the grounded KB 3. If UNSAT → original KB is unsatisfiable (entailment proved)

Problem: if no function symbols, finite ground terms. With function symbols (e.g., Succ(x)), infinitely many ground terms → must enumerate incrementally.

Depth-k propositionalization: only generate terms of depth ≤ k; increase k until UNSAT found or query proved.

Undecidability of FOL

Gödel’s completeness theorem (1930): any valid FOL sentence has a proof of finite length.

Church and Turing (1936): there is no algorithm that decides, for arbitrary FOL sentences, whether they are valid. FOL is semi-decidable: - If KB ⊨ α, a proof will be found in finite time - If KB ⊭ α, the algorithm may run forever

Consequence: we can prove true entailments but cannot always determine non-entailment.

Chapter Roadmap

  1. Unification: matching FOL sentences for direct inference
  2. Generalized Modus Ponens (GMP): lifted version of modus ponens
  3. Forward chaining in FOL: data-driven inference with lifting
  4. Backward chaining in FOL: goal-directed inference (Prolog)
  5. Resolution in FOL: Skolemization + CNF + generalized resolution