EECS 3401 — AI and Logic Prog. — Lecture 7
Adapted from slides of Prof. Yves Lesperance
Vitaliy Batusov
vbatusov@cse.yorku.ca
York University
October 5, 2020
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 1 / 32
Resultion: Unification
Today: Unification in FOL Resolution
Required reading: Russell & Norvig, Chapters 9.1, 9.2, 9.5
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 2 / 32
Unification
Ground clause = a clause with no variables
Finding a pair of complimentary literals {p, ¬p} is trivial in ground
clauses — syntactical identity suffices
But what if we have variables in the clauses?
Can these clauses be resolved? (p(john),q(fred),r(X))
(¬p(Y ), r (susan), r (Y ))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 3 / 32
Unification
Recall: in clausal form, all variables are universally quantified. So, implicitly, the clause
(¬p(Y ), r (susan), r (Y )) represents all clauses like
(¬p(fred ),r (susan), r (fred )) (¬p(john),r (susan), r (john))
…
Thus, there is a “specialization” of this clause that can be resolved with (p(john),q(fred),r(X)).
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 4 / 32
Unification
We want to be able to match conflicting literals, even if they have variables.
This matching process automatically determines whether or not there is a “specialization” that matches.
Don’t want to over-specialize!
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 5 / 32
Consider:
(¬p(X),s(X),q(fred)) (p(Y),r(Y))
Possible resolvants:
(s(john),q(fred),r(john)) {Y = X,X = john} (s(sally),q(fred),r(sally)) {Y = X,X = sally} (s(X),q(fred),r(X)) {Y = X}
The last one is the most general, and the first two are specializations of it
We want to keep the most general clause so that we can use it in future resolution steps
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 6 / 32
Unification
Unification is a mechanism for finding a “most general” matching But first,
A substitution is a finite set of equations of the form (V = t)
where V is a variable and t is a term not containing V . (It might contain other variables)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 7 / 32
Substitutions
We can apply a substitution σ to a formula φ to obtain a new formula φσ by simultaneously replacing every variable mentioned in the left-hand side of the substitution by the right-hand side.
Example:
p(X,g(Y,Z))[X = Y,Y = f(a)] ⇒ p(Y,g(f(a),Z))
Note that the substitutions are not applied sequentially, i.e., the first Y is not subsequently replaced by f (a).
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 8 / 32
Substitutions
We can also compose two substitutions θ and σ to obtain a new substitution θσ.
Let θ = {X1 = s1,X2 = s2,…,Xm = sm} σ = {Y1 = t1,Y2 = t2,…,Yk = tk}
1 Apply σ to each right-hand side of θ and then add all of the equations of σ.
S = {X1 = s1σ,X2 = s2σ,…,Xm = smσ, Y1 = t1,Y2 = t2,…,Yk = tk}
2 Delete from S all identities of the form V = V
3 Delete all equations Yi = si where Yi is equal to one of the Xj in θ
The resulting set S is the composition θσ.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 9 / 32
Composition Example
θ={X=f(Y),Y=Z}, σ={X=a,Y=b,Z=Y}
S ={X=f(Y)σ,Y =Zσ,X=a,Y=b,Z=Y} ={X = f (b), Y = Y , X = a, Y = b, Z = Y } ={X = f (b), Y = Y , X = a, Y = b, Z = Y } ={X = f (b), X = a, Y = b, Z = Y }
θσ ={X = f (b), Y = b, Z = Y }
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 10 / 32
Substitutions
The empty substitution ε = {} is also a legal substitution, and it act as an identity under composition
More importantly, substitutions are associative when applied to formulas:
(φθ)σ = φ(θσ)
Composition is simply a way of converting the sequential application
of a series of substitutions to a single simultaneous substitution
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 11 / 32
Unifiers
A unifier of two formulas φ and ψ is a substitution σ that makes φ and ψ syntactically identical
Not all formulas can be unified — substitutions only affect variables Example: the formulas p(f (X ), a) and p(Y , f (w )) cannot be unified,
since there is no way of making a = f (w ) with a substitution.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 12 / 32
Most General Unifier
A substitution σ if two formulas φ and ψ is a Most General Unifier (MGU) if
1 σ is a unifier
2 For every other unifier θ of φ and ψ there must exist a third
substitution λ such that
θ = σλ.
In other words, σ is a MGU if every other unifier is “more specialized” that σ. The MGU of a pair of formulas φ and ψ is unique up to renaming.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 13 / 32
Most General Unifier
Consider two formulas:
p(f(X),Z), p(Y,a) σ = {Y = f (a), X = a, Z = a} is a unifier:
p(f (X ), Z )σ = p(f (a), a) p(Y , a)σ = p(f (a), a)
But it is not a MGU.
θ = {Y = f (X ), Z = a} is a MGU:
p(f (X ), Z )θ = p(f (X ), a) p(Y , a)θ = p(f (X ), a)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 14 / 32
Most General Unifier
Note: σ=θλwhereλ={X=a}
σ = {Y = f (a), X = a, Z = a} θ = {Y = f (X ), Z = a}
λ = {X =a}
θλ = {Y = f (a), X = a, Z = a}
MGU
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
October 5, 2020
15 / 32
Most General Unifier
The MGU is the “least specialized” way of making clauses with universal variables match (syntactically)
We can find MGUs mechanically
Intuitively, we line up two formulas and find the first sub-expression where they disagree. The pair of sub-expressions where they first disagree is called the disagreement set
The algorithm works by successively fixing disagreements sets until the two formulas become syntactically identical
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 16 / 32
Most General Unifier
To find the MGU of two formulas φ and ψ:
1 k=0;σ0 ={},S0 ={φ,ψ}
2 If Sk contains an identical pair of formulas, then stop and return σk — this is the MGU
3 Else, find the disagreement set Dk = {e1, e2} of Sk
4 If e1 is a variable V and e2 is a term t not containing V (or
vice-versa), then let
σk+1 = σk{V =t} (Compose subst.)
Sk+1 = Sk{V =t} (Apply subst.) and go back to 2.
5 Else: stop. Formulas φ and ψ cannot be unified.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 17 / 32
MGU Example 1
S0 = {p(f(a),g(X));p(Y,Y)} σ0 = {}
D0 ={f(a),Y}
σ1 =σ0{Y=f(a)}={Y=f(a)} S1 ={p(f(a),g(X)){Y=f(a)};
p(Y , Y ){Y = f (a)}} = {p(f (a), g (X )), p(f (a), f (a))}
D1 ={g(X),f(a)}
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
k = 0 Y=f(a) k =1
stop
October 5, 2020
18 / 32
MGU Example 2
S0 = {p(a,X,h(g(Z)));p(Z,h(Y),h(Y))} σ0 = {}
D0 ={a,Z}
σ1 =σ0{Z=a}={Z=a}
S1 ={p(a,X,h(g(a)));p(a,h(Y),h(Y))}
D1 ={X,h(Y)}
σ2 =σ1{X=h(Y)}={Z=a,X=h(Y)}
S2 ={p(a,h(Y),h(g(a)));p(a,h(Y),h(Y))}
D2 = {g(a),Y}
σ3 = σ2{Y =g(a)} = {Z =a, X =h(g(a)), Y =g(a)} S3 ={p(a,h(g(a)),h(g(a)));p(a,h(g(a)),h(g(a)))}
Identical formulas; stop and return σ3 as the MGU Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
k = 0 Z=a k=1 X=h(Y) k =2 Y =g(a) k = 3
October 5, 2020
19 / 32
MGU Example 3
S0 = {p(X,X);p(Y,f(Y))} σ0 = {}
D0 ={X,Y}
σ1 =σ0{X=Y}={X=Y} S1 = {p(Y,Y);p(Y,f(Y))}
D1 ={Y,f(Y)}
Same variable on both sides Stop; cannot be unified
k = 0 X=Y k =1
Y=f(Y)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
October 5, 2020
20 / 32
Non-Ground Resolution
Basic resolution step for non-ground clauses
If we have two clauses
(p,q1,q2,…,qk) and (¬m,r1,r2,…,rn)
and if there exists a MGU σ for p and m, we infer the new clause
(q1σ,…,qkσ,r1σ,…,rnσ)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 21 / 32
Example of Non-Ground Resolution
Clauses:
σ = {X =a} Resolve:
(p(X ), q(g (X ))) and (r (a), q(Z ), ¬p(a))
R[1a,2c]{X =a}(q(g(a)),r(a),q(Z))
The notation here is very useful. R[·,·] means a resolution step; 1a means the first (a-th) literal in the first (1-st) clause; 2c means the third (c-th) literal in the second clause. {X = a} is the substitution applied to make the clashing literals identical.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 22 / 32
Resolution Proof Example
Consider:
Some patients like all doctors. No patient likes any quack. Therefore, no doctor is a quack.
Resolution Step 1: pick symbols to represent these assertions p(X) — X is a patient
d(X) — X is a doctor
q(X) — X is a quack
l(X,Y) — X likes Y
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 23 / 32
Resolution Proof Example
Resolution Step 2: Convert each assertion to a first-order formula Some patients like all doctors
∃X (p(X ) ∧ ∀Y (d (Y ) → l (X , Y ))) No patient likes any quack
∀X∀Y(p(X)∧q(Y) → ¬l(X,Y)) Therefore, no doctor is a quack
¬∃X(d(X) ∧ q(X))
F1
Query
F2
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
October 5, 2020
24 / 32
Resolution Proof Example
Resolution Step 3: Convert to Clausal Form
(p(a)),(¬d(X),l(a,X)) F1 (¬p(Y),¬q(Z),¬l(Y,Z)) F2
(¬d(V ), ¬q(V ))
Query
(d(b)), (q(b))
Negation of Query
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU)
EECS 3401 Lecture 7 October 5, 2020 25 / 32
Resolution Proof Example
Resolution Step 4: Derive an empty clause
p(a)
(¬d(X),l(a,X)) (¬p(Y),¬q(Z),¬l(Y,Z)) d(b)
q(b)
R[1,3a]{Y =a}(¬q(Z),¬l(a,Z)) R[2a,4]{X =b}l(a,b) R[5,6a]{Z=b}¬l(a,b)
R [7, 8]{}()
(1) (2) (3) (4) (5)
(6) (7) (8)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7
October 5, 2020
26 / 32
Answer Extraction
The previous example shows how we can answer true-false questions. With a bit more effort we can also answer “fill-in-the-blanks” questions
As in Prolog, we use free variables in the query where we want the fill-in-the-blanks. We simply need to keep track of the binding that these variables received in proving the query.
parent(art,jon) — is art one of jon’s parents? (Yes/No) parent(X,jon) — who is one of jon’s parents? (Fill-in-the-blanks)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 27 / 32
Answer Extraction
A simple bookkeeping device is to use a predicate symbol answer (X , Y , . . .) to keep track of the bindings automatically
To answer the query parent(X,jon), we construct the clause (¬parent(X,jon),answer(X))
Now we perform resolution until we obtain a clause consisting of only answer literals. (Previously we stopped at empty clauses)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 28 / 32
Answer Extraction Example 1
1 father(art,jon)
2 father (bob, kim)
3 (¬father(Y,Z),parent(Y,Z))
4 (¬parent(X,jon),answer(X))
Proof:
5 R[4,3b]{Y =X,Z =jon}(¬father(X,jon),answer(X))
6 R [5, 1]{X = art }(answer (art )) And we have an explicit answer.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 29 / 32
Answer Extraction Example 2
1 (father(art, jon), father(bob, jon))
2 father (bob, kim)
3 (¬father(Y,Z),parent(Y,Z))
4 (¬parent(X,jon),answer(X))
Proof:
5 R[4,3b]{Y =X,Z =jon}(¬father(X,jon),answer(X))
6 R[5, 1a]{X =art}(father(bob, jon), answer(art))
7 R[6,3b]{Y=bob,Z=jon}(parent(bob,jon),answer(art))
8 R[7, 4]{X =bob}(answer(bob), answer(art))
A disjunctive answer: either bob or art is a parent of jon.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 30 / 32
Prolog
The Prolog search mechanism (without not and ! ) is simply an instance of resolution, except
Clauses are Horn (only one positive literal)
Prolog uses a specific depth-first strategy when searching for a proof (rules are used first-mentioned-first-used, literals are resolved away left-to-right)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 31 / 32
End of Lecture
Next time: SLDNF Resolution
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 7 October 5, 2020 32 / 32