Unification We can get the inference immediately if we can find a substitution such that King(x)and Greedy(x)match King(John)and Greedy(y) 0=[x/John,y/John}works ·Unify(a,β)=日ifa0=B6 p q 0 Knows(John,x)Knows(John,Jane) [x/Jane)) Knows(John,x)Knows(y,OJ) Knows(John,x)Knows(y,Mother(y)) Knows(John,x)Knows(x,OJ)Unification • We can get the inference immediately if we can find a substitution θ such that King(x) and Greedy(x) match King(John) and Greedy(y) • θ = {x/John,y/John} works • Unify(α,β) = θ if αθ = βθ • p q θ Knows(John,x) Knows(John,Jane) {x/Jane}} Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)