Knowledge Repn. & Reasoning Lec. #6: First-Order InferenceTodayResolution Theorem ProvingSlide 4Slide 5First-Order ResolutionSlide 7Resolution in ActionSlide 9Slide 10First-Order Resolution RuleUnificationSlide 13Slide 14Slide 15Finding the MGUSlide 17Slide 18Slide 19Slide 20Slide 21Finding the MGU: another exampleSlide 23Slide 24Slide 25Slide 26Slide 27Correctness of FOL ResolutionSimple Efficiency ImprovementsSlide 30Properties of ResolutionRelated to FOL ResolutionSummary So FarSituation CalculusSlide 35NotationsNext TimeKnowledge Repn. & ReasoningLec. #6: First-Order InferenceUIUC CS 498: Section EAProfessor: Eyal AmirFall Semester 2004Today•Until now: –First-order logic basics–Clausal form for FOL•Resolution refutation for FOL•Application du jour: Temporal Reasoning•Applications we will not touch–Spatial reasoning, formal verification, mathematics, planning, NLP, …Resolution Theorem Proving•Given:–KB – a set of first-order sentences–Query Q – a logical sentence•Calling procedure:1. Add Q to KB2. Convert KB into clausal form3. Run theorem prover. If we prove contradiction, return T.Resolution Theorem Proving1. Add Q to KB2. Convert KB into clausal form3. Run theorem prover. If we prove contradiction, return T. Deduction theorem:KB Q iff KB Q FALSE╨╨Resolution Theorem Proving1. Add Q to KB2. Convert KB into clausal form3. Run theorem prover. If we prove contradiction, return T. Deduction theorem:KB Q iff KB Q FALSE╨╨First-Order Resolution•Resolution inference rule:C1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}First-Order Resolution•Resolution algorithm (saturation):1. While there are unresolved C1,C2:(1) Select C1, C2 in KB(2) If C1, C2 are resolvable, resolve them into a new clause C3(3) Add C3 to KB(4) If C3={ }return T.2. STOPC1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}Resolution in Action)()()()()()()()()()()()()()()()(AaBfAcBfCercwfCezaBfycAatfsaxcxaOn boardNegated QueryKBC1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}Resolution in Action)()()()()()()()()()()()()()()()(AaBfAcBfCercwfCezaBfycAasfsaxcxaOn boardNegated QueryKBC1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}First-Order Resolution•Resolution algorithm (saturation):1. While there are unresolved C1,C2:(1) Select C1, C2 in KB(2) If C1, C2 are resolvable, resolve them into a new clause C3(3) Add C3 to KB(4) If C3={ }return T.2. STOPC1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}First-Order Resolution Rule(2) If C1, C2 are resolvable, resolve them into a new clause C3If C1,C2 have two literals l1,l2 with same predicates (P) and opposite polarity, andIf l1= P(t1,…,tk), l2= P(s1,…,sk), unifiablewith mgu (most general unifier) {r1,…,rn},then…C1: P(t1,…,tk) C1’(t1,…,tk)C2: P(s1,…,sk) C2’(s1,…,sk)mgu(<t1,…,tk>,<s1,…,sk>) = {r1,…,rn}--------------------------------------------C3: (C1’ C2’) {r1,…,rn}Unification…P(t1,…,tk),P(s1,…,sk), unifiable with mgu (most general unifier) σ={r1,…rk}•Substitution: replace vars. by terms–Term: constant, variable, or a function of terms•Composition of substitutions{x/g(w,v)} {w/A,v/f(B,z)} ={x/g(A,f(B,z),w/A,v/f(B,z)}(P(x) v Q(f(x)) v P(g(B,x)) v P(f(y))) {x/B,y/z}(P(B) v Q(f(B)) v P(g(B,B)) v P(f(z))){x/B,y/z} {x/B,y/z,x/w} {x/B,y/z,z/w}Unification•Unification: find a substitution σ for•C1: P(t1,…,tk) C1’(t1,…,tk)•C2: P(s1,…,sk) C2’(s1,…,sk)such that P(t1,…,tk)σ = P(s1,…,sk)σP(A,y,g(x,y)){y/f(A)} = P(z,f(z),g(x,f(w))){z/A,w/A}σ={y/f(A),z/A,w/A}P(A,y,g(x,y)){y/f(w)} = P(z,f(w),g(x,f(w))){z/A}σ={y/f(w),z/A}Most general unifierUnification•Substitution σ1 more general than σ2 if there is substitution γ such thatσ1 γ = σ2P(A,y,g(x,y)){y/f(A)} = P(z,f(z),g(x,f(w))){z/A,w/A}σ={y/f(A),z/A,w/A}P(A,y,g(x,y)){y/f(w)} = P(z,f(w),g(x,f(w))){z/A}σ={y/f(w),z/A}Most general unifierUnification•Substitution σ1 more general than σ2 if there is substitution γ such thatσ1 γ = σ2σ2={y/f(A),z/A,w/A}σ1={y/f(w),z/A}Most general unifierγ={w/A}Finding the MGUProcedure MGU(x,y)1. If x=y, return { }2. If x or y are vars., return MGUvar(x,y)3. If x or y are const.,or Len(x)=/=Len(y), return F.4. σ ← { }; For i ← 1 to Len(x)1. s ← MGU(part(i,x),part(i,y)); if s=F, return F.2. σ ← compose(σ,s); x ← subst(x,σ); y ← subst(y,σ); 5. Return σx = P(A,y,g(x,y)) y = P(z,f(w),g(v,w))Finding the MGUProcedure MGU(x,y)1. If x=y, return { }2. If x or y are vars., return MGUvar(x,y)3. If x or y are const.,or Len(x)=/=Len(y), return F.4. σ ← { }; For i ← 1 to Len(x)1. s ← MGU(part(i,x),part(i,y)); if s=F, return F.2. σ ← compose(σ,s); x ← subst(x,σ); y ← subst(y,σ); 5. Return σx = P(A,y,g(x,y)) y = P(z,f(w),g(v,w))Finding the MGUProcedure MGU(x,y)1. If x=y, return { }2. If x or y are vars., return MGUvar(x,y)3. If x or y are const.,or Len(x)=/=Len(y), return F.4. σ ← { }; For i ← 1 to Len(x)1. s ← MGU(part(i,x),part(i,y)); if s=F, return F.2. σ ← compose(σ,s); x ← subst(x,σ); y ← subst(y,σ); 5. Return σx = P(A,y,g(x,y)) y = P(z,f(w),g(v,w))Finding the MGUProcedure MGU(x,y)1. If x=y, return { }2. If x or y are vars., return MGUvar(x,y)3. If x or y are const.,or Len(x)=/=Len(y), return F.4. σ ← { }; For i ← 1 to Len(x)1. s ← MGU(part(i,x),part(i,y)); if s=F, return F.2. σ ← compose(σ,s); x ← subst(x,σ); y ← subst(y,σ); 5. Return σx = P(A,y,g(x,y)) y = P(z,f(w),g(v,w))Finding the MGUProcedure MGU(x,y)1. If x=y, return { }2. If x or y are vars.,
View Full Document
Unlocking...