Unification and Generalized Modus Ponens

Unification

Unification finds a substitution θ that makes two FOL expressions identical.

UNIFY(p, q) returns θ such that SUBST(θ, p) = SUBST(θ, q), or failure

Examples

Expression 1	Expression 2	Unifier θ
`Knows(John, x)`	`Knows(John, Jane)`	`{x/Jane}`
`Knows(John, x)`	`Knows(y, Bill)`	`{x/Bill, y/John}`
`Knows(John, x)`	`Knows(x, Elizabeth)`	failure (x can’t be both)
`Knows(John, x)`	`Knows(John, Mother(John))`	`{x/Mother(John)}`

Most General Unifier (MGU)

Many substitutions may unify two expressions. The most general unifier (MGU) is the one that makes the fewest commitments (most specific bindings):

{x/John, y/John} unifies Knows(x,y) and Knows(y,x)
But so does {x/John, y/John}, {x/Bill, y/Bill}, etc.
MGU: {x/y} (or {y/x}) — most general

The Occur Check

Problem: UNIFY(x, F(x)) — should this fail?

If we allow x = F(x), then x = F(F(F(...))) — infinite structure.

Occur check: unification fails if the variable appears in the term it would be bound to.

Prolog omits the occur check for efficiency (can create circular structures but usually fine in practice).

Unification Algorithm (UNIFY)

function UNIFY(x, y, θ) returns substitution or failure
    if θ = failure then return failure
    if x = y then return θ
    if VARIABLE?(x) then return UNIFY-VAR(x, y, θ)
    if VARIABLE?(y) then return UNIFY-VAR(y, x, θ)
    if COMPOUND?(x) and COMPOUND?(y) then
        return UNIFY(ARGS(x), ARGS(y), UNIFY(OP(x), OP(y), θ))
    if LIST?(x) and LIST?(y) then
        return UNIFY(REST(x), REST(y), UNIFY(FIRST(x), FIRST(y), θ))
    return failure

function UNIFY-VAR(var, x, θ)
    if {var/val} ∈ θ then return UNIFY(val, x, θ)
    if {x/val} ∈ θ then return UNIFY(var, val, θ)
    if OCCUR-CHECK?(var, x) then return failure
    return θ ∪ {var/x}

Generalized Modus Ponens (GMP)

Lifts modus ponens to FOL using unification:

For sentences p₁', p₂', ..., pₙ' and (p₁ ∧ p₂ ∧ ... ∧ pₙ → q):

If there exists θ such that SUBST(θ, pᵢ') = SUBST(θ, pᵢ) for all i, then conclude:

SUBST(θ, q)

Example

KB:
  (1)  King(John)
  (2)  Greedy(John)
  (3)  ∀x King(x) ∧ Greedy(x) → Evil(x)

GMP with θ = {x/John}:
  p₁' = King(John),   p₁ = King(x)        -- match with θ
  p₂' = Greedy(John), p₂ = Greedy(x)      -- match with θ
  q   = Evil(x)

Conclude: SUBST({x/John}, Evil(x)) = Evil(John)

Standardize Apart

Before unification, rename variables in each sentence to be unique (avoid variable clashes):

∀x P(x) → Q(x) used twice: rename second copy to ∀x2 P(x2) → Q(x2).

This standardization prevents accidental variable capture.

Why Lifting > Propositionalization

Propositionalization: instantiate ∀x King(x) ∧ Greedy(x) → Evil(x) for every constant → O(n) instances.

Lifting (GMP + unification): match the rule directly against known facts → derive only what’s needed. No unnecessary instantiation.

Practical impact: for a KB with 1000 constants and 100 rules, propositionalization generates 100,000 ground sentences. GMP generates only what’s entailed by the query.