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 0 Knows(John,x)Knows(John,Jane) [x/Jane)} Knows(John,x)Knows(y,OJ) x/OJ,y/John)) 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) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) Knows(John,x) Knows(x,OJ) • Standardizing apart eliminates overlap of variables, e.g
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) [x/OJ,y/John)) Knows(John,x)Knows(y,Mother(y)) (y/John,x/Mother(John)) 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) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}} Knows(John,x) Knows(x,OJ) • Standardizing apart eliminates overlap of variables, e.g
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 6 Knows(John,x)Knows(John,Jane) [x/Jane)) Knows(John,x)Knows(y,OJ) {x/OJ,y/John)) Knows(John,x)Knows(y,Mother(y)) (y/John,x/Mother(John)) Knows(John,x)Knows(x,OJ) (fail)
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) {x/OJ,y/John}} Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}} Knows(John,x) Knows(x,OJ) {fail}
Unification To unify Knows(John,x)and Knows(y,z), 0=(y/John,x/z or 0=[y/John,x/John,z/John} The first unifier is more general than the second. ● There is a single most general unifier(MGU)that is unique up to renaming of variables. MGU={y/John,x/z
Unification • To unify Knows(John,x) and Knows(y,z), • θ = {y/John, x/z } or θ = {y/John, x/John, z/John} • The first unifier is more general than the second. • • There is a single most general unifier (MGU) that is unique up to renaming of variables. • MGU = { y/John, x/z }
The unification algorithm function UNIFY(,y.0)returns a substitution to make x and y identical inputs:z,a variable,constant,list,or compound y,a variable,constant,list,or compound 0,the substitution built up so far if0=failure then return failure else if z=y then return 0 else if VARIABLE?(z)then return UNIFY-VAR(z,y,0) else if VARIABLE?(y)then return UNIFY-VAR(y.Z,0) else if CoMPOUND?(z)and COMPOUND?(y)then return UNIFY(ARGS[],ARGS[y],UNIFY(OP[a].OP[y],0)) else if LIST?()and LIST?(y)then return UNIFY(REST[a],REST[y],UNIFY(FIRST[],FIRST[y],0)) else return failure
The unification algorithm