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,B)=0 if a0=B0 ∂ 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(E,OJ) Chapter9 11
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) Chapter 9 11
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={/John,y/John}works UNIFY(a,B)=0 if a0=30 q le Knows(John,x)Knows(John,Jane) {x/Janey Knows(John,x) Knows(y,OJ) /OJ,y/John} Knows(John,x) Knows(y,Mother(y)】 Knows(John,x)Knows(x,OJ) Chapter 9 12
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) Chapter 9 12
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,B)=0 if a0=B0 q Knows(John,x) Knows(John,Jane x/Jane Knows(John,x) Knows(y,OJ)） z/OJ,y/John Knows(John,x) Knows(y,Mother(y)) y/John,x/Mother(John)} Knows(John,x)Knows(,OJ) Chapter9 13
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) Chapter 9 13
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,B)=0 if a0=B0 q le Knows(John,x)Knows(John,Jane) ix/Janet 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 Standardizing apart eliminates overlap of variables,e.g.,Knows(,OJ) Chapter 9 14
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 Standardizing apart eliminates overlap of variables, e.g., Knows(z17, OJ) Chapter 9 14
Generalized Modus Ponens (GMP) p1',p2',,pn',(p1Ap2∧…Apn→q where pi=p:e for all i go pl'is King(John) pi is King(x) p2'is Greedy(y) p2 is Greedy(x) 0 is {x/John,y/John}q is Evil() ge is Evil(John) GMP used with KB of definite clauses(exactly one positive literal) All variables assumed universally quantified Chapter9 15
Generalized Modus Ponens (GMP) p10, p20, . . . , pn0, (p1 ∧ p2 ∧ . . . ∧ pn ⇒ q) qθ where pi0θ = piθ for all i p10 is King(John) p1 is King(x) p20 is Greedy(y) p2 is Greedy(x) θ is {x/John, y/John} q is Evil(x) qθ is Evil(John) GMP used with KB of definite clauses (exactly one positive literal) All variables assumed universally quantified Chapter 9 15