Resolution:brief summary Resolution proof:definite clauses Full first-order version: GVV,m1V…Vm (...vu-ivG-iv......Vmj-1VmmV...vm.8 where UNIFY(u）=B. For example Apply resolution steps to CNF(K BA):complete for FOL Conversion to CNF 1.Eliminate biconditionals and implications 2.Moe一inwards:Vx,p=3rg.3r.p三Vr: Conversion to CNF contd. 3.Standardize: x日Animal(A一Loves(r,w】V日：Lots(&.x月 4 Skol Animal(F(zA-Lored，Fu VLoves(G(r.) 5.Drop universal quantifiers: 【Animal(Fx）A-Loes(z.Fx)月Loves(Gzl.r）Resolution: brief summary Full first-order version: `1 ∨ · · · ∨ `k, m1 ∨ · · · ∨ mn (`1 ∨ · · · ∨ `i−1 ∨ `i+1 ∨ · · · ∨ `k ∨ m1 ∨ · · · ∨ mj−1 ∨ mj+1 ∨ · · · ∨ mn)θ where Unify(`i , ¬mj) = θ. For example, ¬Rich(x) ∨ Unhappy(x) Rich(Ken) Unhappy(Ken) with θ = {x/Ken} Apply resolution steps to CNF(KB ∧ ¬α); complete for FOL Chapter 9 43 Conversion to CNF Everyone who loves all animals is loved by someone: ∀ x [∀ y Animal(y) ⇒ Loves(x, y)] ⇒ [∃ y Loves(y, x)] 1. Eliminate biconditionals and implications ∀ x [¬∀ y ¬Animal(y) ∨ Loves(x, y)] ∨ [∃ y Loves(y, x)] 2. Move ¬ inwards: ¬∀ x, p ≡ ∃ x ¬p, ¬∃ x, p ≡ ∀ x ¬p: ∀ x [∃ y ¬(¬Animal(y) ∨ Loves(x, y))] ∨ [∃ y Loves(y, x)] ∀ x [∃ y ¬¬Animal(y) ∧ ¬Loves(x, y)] ∨ [∃ y Loves(y, x)] ∀ x [∃ y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃ y Loves(y, x)] Chapter 9 44 Conversion to CNF contd. 3. Standardize variables: each quantifier should use a different one ∀ x [∃ y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃ z Loves(z, x)] 4. Skolemize: a more general form of existential instantiation. Each existential variable is replaced by a Skolem function of the enclosing universally quantified variables: ∀ x [Animal(F(x)) ∧ ¬Loves(x, F(x))] ∨ Loves(G(x), x) 5. Drop universal quantifiers: [Animal(F(x)) ∧ ¬Loves(x, F(x))] ∨ Loves(G(x), x) 6. Distribute ∧ over ∨: [Animal(F(x)) ∨ Loves(G(x), x)] ∧ [¬Loves(x, F(x)) ∨ Loves(G(x), x)] Chapter 9 45 Resolution proof: definite clauses American(West) Missile(M1) Missile(M1) Owns(Nono,M1) Enemy(Nono,America) Enemy(Nono,America) Hostile(z) Criminal(x) L Sells(x,y,z) L Weapon(y) L American(x) L > > > > Missile(x) Weapon(x) L > Missile(x) Sells(West,x,Nono) L Owns(Nono,x) > L > Enemy(x,America) Hostile(x) L > Sells(West,y,z) L Weapon(y) L American(West) L > > Hostile(z) > L Sells(West,y,z) L Weapon(y) L > Hostile(z) > L Sells(West,y,z) > L Hostile(z) L > L Missile(y) Hostile(z) L > L Sells(West,M1,z) > > LHostile(Nono) LOwns(Nono,M1) LMissile(M1) > LHostile(Nono) LOwns(Nono,M1) LHostile(Nono) Criminal(West) L Chapter 9 46