Skolemization, Most General Unifiers,
First-Order Resolution
Torsten Hahmann
CSC 384, University of Toronto
March 07, 2011
Skolemization
Conversion of sentences FOL to CNF requires skolemization.
Skolemization: remove existential quantifiers by introducing new
function symbols.
How: For each existentially quantified variable introduce a n-place
function where n is the number of previously appearing universal
quantifiers.
Special case: introducing constants (trivial functions: no previous
universal quantifier).
Skolemization - Example 1
I Every philosopher writes at least one book.
∀x[Philo(x) → ∃y [Book(y ) ∧ Write(x, y )]]
Skolemization - Example 1
I Every philosopher writes at least one book.
∀x[Philo(x) → ∃y [Book(y ) ∧ Write(x, y )]]
I Eliminate Implication:
∀x[¬Philo(x) ∨ ∃y [Book(y ) ∧ Write(x, y )]]
Skolemization - Example 1
I Every philosopher writes at least one book.
∀x[Philo(x) → ∃y [Book(y ) ∧ Write(x, y )]]
I Eliminate Implication:
∀x[¬Philo(x) ∨ ∃y [Book(y ) ∧ Write(x, y )]]
I Skolemize: substitute y by g (x)
∀x[¬Philo(x) ∨ [Book(g (x)) ∧ Write(x, g (x))]]
Skolemization - Example 2
I All students of a philosopher read one of their teacher’s books.
∀x∀y [Philo(x) ∧ StudentOf (y , x) →
∃z[Book(z) ∧ Write(x, z) ∧ Read(y , z)]]
Skolemization - Example 2
I All students of a philosopher read one of their teacher’s books.
∀x∀y [Philo(x) ∧ StudentOf (y , x) →
∃z[Book(z) ∧ Write(x, z) ∧ Read(y , z)]]
I Eliminate Implication:
∀x∀y [¬Philo(x) ∨ ¬StudentOf (y , x) ∨ ∃z[Book(z) ∧
Write(x, z) ∧ Read(y , z)]]
Skolemization - Example 2
I All students of a philosopher read one of their teacher’s books.
∀x∀y [Philo(x) ∧ StudentOf (y , x) →
∃z[Book(z) ∧ Write(x, z) ∧ Read(y , z)]]
I Eliminate Implication:
∀x∀y [¬Philo(x) ∨ ¬StudentOf (y , x) ∨ ∃z[Book(z) ∧
Write(x, z) ∧ Read(y , z)]]
I Skolemize: substitute z by h(x, y )
∀x∀y [¬Philo(x) ∨ ¬StudentOf (y , x) ∨ [Book(h(x, y )) ∧
Write(x, h(x, y )) ∧ Read(y , h(x, y ))]]
Skolemization - Example 3
I There exists a philosopher with students.
∃x∃y [Philo(x) ∧ StudentOf (y , x)]
Skolemization - Example 3
I There exists a philosopher with students.
∃x∃y [Philo(x) ∧ StudentOf (y , x)]
I Skolemize: substitute x by a and y by b
Philo(a) ∧ StudentOf (b, a)
Most General Unifier
Least specialized unification of two clauses.
We can compute the MGU using the disagreement set
Dk = {e1 , e2 }: the pair of expressions where two clauses first
disagree.
REPEAT UNTIL no more disagreement → found MGU.
IF either e1 or e2 is a variable V and the other is some term (or a
variable) t, then choose V = t as substitution.
Then substitute to obtain Sk+1 and find disagreement set Dk+1 .
ELSE unification is not possible.
MGU - Example 1
Find the MGU of p(f (a), g (X )) and p(Y , Y ):
I S0 = {p(f (a), g (X )) ; p(Y , Y )}
MGU - Example 1
Find the MGU of p(f (a), g (X )) and p(Y , Y ):
I S0 = {p(f (a), g (X )) ; p(Y , Y )}
I D0 = {f (a), Y }
I σ = {Y = f (a)}
MGU - Example 1
Find the MGU of p(f (a), g (X )) and p(Y , Y ):
I S0 = {p(f (a), g (X )) ; p(Y , Y )}
I D0 = {f (a), Y }
I σ = {Y = f (a)}
I S1 = {p(f (a), g (X )) ; p(f (a), f (a))}
MGU - Example 1
Find the MGU of p(f (a), g (X )) and p(Y , Y ):
I S0 = {p(f (a), g (X )) ; p(Y , Y )}
I D0 = {f (a), Y }
I σ = {Y = f (a)}
I S1 = {p(f (a), g (X )) ; p(f (a), f (a))}
I D1 = {g (X ), f (a)}
MGU - Example 1
Find the MGU of p(f (a), g (X )) and p(Y , Y ):
I S0 = {p(f (a), g (X )) ; p(Y , Y )}
I D0 = {f (a), Y }
I σ = {Y = f (a)}
I S1 = {p(f (a), g (X )) ; p(f (a), f (a))}
I D1 = {g (X ), f (a)}
I no unification possible!
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
I S2 = {p(a, h(Y ), h(g (a))) ; p(a, h(Y ), h(Y ))}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
I S2 = {p(a, h(Y ), h(g (a))) ; p(a, h(Y ), h(Y ))}
I D2 = {g (a), Y }
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
I S2 = {p(a, h(Y ), h(g (a))) ; p(a, h(Y ), h(Y ))}
I D2 = {g (a), Y }
I σ = {Z = a, X = h(Y ), Y = g (a)}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
I S2 = {p(a, h(Y ), h(g (a))) ; p(a, h(Y ), h(Y ))}
I D2 = {g (a), Y }
I σ = {Z = a, X = h(Y ), Y = g (a)}
I S3 = {p(a, h(g (a)), h(g (a))) ; p(a, h(g (a)), h(g (a)))}
MGU - Example 2
I S0 = {p(a, X , h(g (Z ))) ; p(Z , h(Y ), h(Y ))}
I D0 = {a, Z }
I σ = {Z = a}
I S1 = {p(a, X , h(g (a))) ; p(a, h(Y ), h(Y ))}
I D1 = {X , h(Y )}
I σ = {Z = a, X = h(Y )}
I S2 = {p(a, h(Y ), h(g (a))) ; p(a, h(Y ), h(Y ))}
I D2 = {g (a), Y }
I σ = {Z = a, X = h(Y ), Y = g (a)}
I S3 = {p(a, h(g (a)), h(g (a))) ; p(a, h(g (a)), h(g (a)))}
I No disagreement
⇒ σ = {Z = a, X = h(Y ), Y = g (a)} is MGU
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
I D0 = {X , Y }
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
I D0 = {X , Y }
I σ = {X = Y }
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
I D0 = {X , Y }
I σ = {X = Y }
I S1 = {p(Y , Y ) ; p(Y , f (Y ))}
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
I D0 = {X , Y }
I σ = {X = Y }
I S1 = {p(Y , Y ) ; p(Y , f (Y ))}
I D1 = {Y , f (Y )}
MGU - Example 3
I S0 = {p(X , X ) ; p(Y , f (Y ))}
I D0 = {X , Y }
I σ = {X = Y }
I S1 = {p(Y , Y ) ; p(Y , f (Y ))}
I D1 = {Y , f (Y )}
I no unification possible!
Full example problem
Given the following sentences, answer the question ‘What is
connected to the Galbraith building?’ using resolution with answer
extraction:
Connected is a binary symmetric relation.
An object X is part of another object Y iff everything X is
connected to, Y is also connected to.
Room GB221 is part of Galbraith building.
Room GB221 is connected to itself.
Full example problem - Representation in FOL
(a) Represent these sentences in first order logic.
Connected is a binary symmetric relation.
An object X is part of another object Y iff everything X is
connected to, Y is also connected to.
Room GB221 is part of Galbraith building.
Room GB221 is connected to itself.
Full example problem - Representation in FOL
I Connected is a symmetric relation.
(∀X , Y ) connected(X , Y ) ⊃ connected(Y , X )
Full example problem - Representation in FOL
I An object X is part of another object Y iff everything X is
connected to, Y is also connected to.
(∀X , Y ) (part(X , Y ) ≡ ((∀Z ) connected(Z , X ) ⊃
connected(Z , Y )))
Full example problem - Representation in FOL
I Room GB221 is part of Galbraith building.
part(gb221, galbraith)
Full example problem - Representation in FOL
I Room GB221 is connected to itself.
connected(gb221, gb221)
Full example problem - CNF Conversion
(b) Convert the formulas to clausal form. Indicate any Skolem
functions or constants used.
(∀X , Y ) connected(X , Y ) ⊃ connected(Y , X )
(∀X , Y ) part(X , Y ) ≡ (∀Z ) connected(Z , X ) ⊃ connected(Z , Y )
part(gb221, galbraith)
connected(gb221, gb221)
Full example problem - CNF Conversion
I (∀X , Y ) connected(X , Y ) ⊃ connected(Y , X )
[−connected(X , Y ), connected(Y , X )]
Full example problem - CNF Conversion
I (∀X , Y ) part(X , Y ) ≡ (∀Z ) connected(Z , X ) ⊃
connected(Z , Y )
→: [−part(X , Y ), −connected(Z , X ), connected(Z , Y )]
←: [part(X , Y ), connected(f (X , Y ), X )]
[part(X , Y ), −connected(g (X , Y ), Y )]
Full example problem - CNF Conversion
I part(gb221, galbraith)
[part(gb221, galbraith)]
Full example problem - CNF Conversion
I connected(gb221, gb221)
[connected(gb221, gb221)]
Full example problem - Goal
(c) Convert the negation of the statement ‘What is connected to
the Galbraith building?’ to clause form (using an answer literal).
I FOL: (∃X ) connected(galbraith, X )
Full example problem - Goal
(c) Convert the negation of the statement ‘What is connected to
the Galbraith building?’ to clause form (using an answer literal).
I FOL: (∃X ) connected(galbraith, X )
I negate goal!! (¬∃X ) connected(galbraith, X )
Full example problem - Goal
(c) Convert the negation of the statement ‘What is connected to
the Galbraith building?’ to clause form (using an answer literal).
I FOL: (∃X ) connected(galbraith, X )
I negate goal!! (¬∃X ) connected(galbraith, X )
I CNF with answer literal: (∀X ) ¬connected(galbraith, X )
[−connected(galbraith, X ), ans(X )]
Full example problem - Resolution
(d) Answer the question using resolution and answer extraction.
Use the notation developed in class: every new clause must be
labeled by the resolution step that was used to generate it. For
example, a clause labeled R[4c, 1d]x = a, y = f(b) means that it
was generated by resolving literal c of clause 4 against literal d of
clause 1, using the MGU x = a, y = f(b).
Our clauses:
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
Full example problem - Resolution
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
Full example problem - Resolution
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
8. R[7a, 1b] {S = galbraith, R = U}
[−connected(A, galbraith), ans(A)]
Full example problem - Resolution
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
8. R[7a, 1b] {S = galbraith, R = U}
[−connected(A, galbraith), ans(A)]
9. R[8a, 2c] {V = A, U = galbraith}
[−part(T , galbraith), −connected(A, T ), ans(A)]
Full example problem - Resolution
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
8. R[7a, 1b] {S = galbraith, R = U}
[−connected(A, galbraith), ans(A)]
9. R[8a, 2c] {V = A, U = galbraith}
[−part(T , galbraith), −connected(A, T ), ans(A)]
10. R[9a, 5] {T = gb221}
[−connected(A, gb221), ans(A)]
Full example problem - Resolution
1. [−connected(R, S), connected(S, R)]
2. [−part(T , U), −connected(V , T ), connected(V , U)]
3. [part(W , X ), connected(f (W , X ), W )]
4. [part(Y , Z ), −connected(g (Y , Z ), Z )]
5. [part(gb221, galbraith)]
6. [connected(gb221, gb221)]
7. [−connected(galbraith, A), ans(A)]
8. R[7a, 1b] {S = galbraith, R = U}
[−connected(A, galbraith), ans(A)]
9. R[8a, 2c] {V = A, U = galbraith}
[−part(T , galbraith), −connected(A, T ), ans(A)]
10. R[9a, 5] {T = gb221}
[−connected(A, gb221), ans(A)]
11. R[10a, 6] {A = gb221}
[ans(gb221)]
