Unification We can get the inference immediately if we can find a substitution 0 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 Knows(John,x)Knows(John,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) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ)