1ApplicationsComputational Logic Lecture 11Michael Genesereth Autumn 20092PlanFirst Lecture - Resolution PreliminariesUnificationRelational Clausal FormSecond Lecture - Resolution PrincipleResolution Principle and FactoringResolution Theorem ProvingThird Lecture - Resolution Applications Theorem ProvingAnswer ExtractionResidueFourth Lecture - Resolution StrategiesElimination Strategies (tautology elimination, subsumption, …)Restriction Strategies (ancestry filtering, set of support, …)23Determining Logical EntailmentTo determine whether a set Δ of sentences logically entails aclosed sentence ϕ, rewrite Δ∪{¬ϕ} in clausal form and try toderive the empty clause.4ExampleShow that (p(x) ⇒ q(x)) and p(a) logically entail ∃z.q(z).1. {¬p(x),q(x)} Premise2. {p(a)} Premise3. {¬q(z)} Goal4. {¬p(z)} 1,35. {} 2, 435Alternate MethodBasic Method: To determine whether a set Δ ofsentences logically entails a closed sentence ϕ,rewrite Δ∪{¬ϕ} in clausal form and try to derive theempty clause.Alternate Method: To determine whether a set Δ ofsentences logically entails a closed sentence ϕ ,rewrite Δ∪{ϕ ⇒ goal} in clausal form and try toderive goal.Intuition: The sentence (ϕ ⇒ goal) is equivalent tothe sentence (¬ϕ ∨ goal).6ExampleShow that (p(x) ⇒ q(x)) and p(a) logically entail∃z.q(z).1. {¬p(x),q(x)} p(x) ⇒ q(x)2. {p(a)} p(a)3. {¬q(z),goal} ∃z.q(z) ⇒ goal4. {¬p(z), goal} 1,35. {goal} 2, 447Answer Extraction MethodAlternate Method for Logical Entailment: Todetermine whether a set Δ of sentences logicallyentails a closed sentence ϕ , rewrite Δ∪{ϕ ⇒ goal} inclausal form and try to derive goal.Method for Answer Extraction: To get values for freevariables ν1,…,νn in ϕ for which Δ logically entails ϕ,rewrite Δ∪{ϕ ⇒ goal(ν1,…,νn)} in clausal form andtry to derive goal(ν1,…,νn).Intuition: The sentence (q(z) ⇒ goal(z)) says that,whenever, z satisfies q, it satisfies the “goal”.8ExampleGiven (p(x) ⇒ q(x)) and p(a), find a term τ such thatq(τ) is true.1. {¬p(x),q(x)} p(x) ⇒ q(x)2. {p(a)} p(a)3. {¬q(z),goal(z)} q(z) ⇒ goal(z)4. {¬p(z), goal(z)} 1,35. {goal(a)} 2, 459ExampleGiven (p(x) ⇒ q(x)) and p(a) and p(b), find a term τsuch that q(τ) is true.€ 1. {¬p(x),q(x)} p (x) ⇒ q(x)2. {p(a)} p (a)3. { p(b)} p(b)4. {¬q(z), goal(z)} q(z) ⇒ goal(z)5. {¬p(z), goal(z)} 1, 46. {goal(a)} 2,57. {goal(b)} 3,510ExampleGiven (p(x) ⇒ q(x)) and (p(a) ∨ p(b)), find a term τsuch that q(τ) is true.1. {¬p(x),q(x)} p(x) ⇒ q(x)2. {p(a), p(b)} p(a) ∨ p(b)3. {¬q(z),goal(z)} q(z) ⇒ goal(z)4. {¬p(z), goal(z)} 1,35. {p(b), goal(a)} 2,46. {goal(a),goal(b)} 4,5611KinshipArt is the parent of Bob and Bud.Bob is the parent of Cal and Coe.A grandparent is a parent of a parent.p(art,bob)p(art,bud)p(bob,cal)p(bob,coe)p(x , y) ∧ p(y, z) ⇒ g(x, z)12Is Art the Grandparent of Coe?1. {p(art,bob)} p(art, bob)2. {p(art,bud)} p(art, bud)3. {p(bob, cal)} p(bob,cal)4. {p(bob,coe)} p(bob,coe)5. {¬p(x, y),¬p(y,z), g(x, z)} p(x , y) ∧ p(y, z) ⇒ g(x,z)6. {¬g(art,coe), goal} g(art, coe) ⇒ goal7. {¬p(art, y),¬p(y, coe), goal} 5,68. {¬p(bob,coe), goal} 1, 79. {goal} 4,8713Who is the Grandparent of Coe?1. {p(art,bob)} p(art,bob)2. {p(art,bud)} p(art,bud)3. {p(bob, cal)} p(bob,cal)4. {p(bob,coe)} p(bob,coe)5. {¬p(x, y),¬p(y,z), g(x, z)} p(x, y) ∧ p(y,z) ⇒ g(x, z)6. {¬g(x,coe), goal(x)} g(x,coe) ⇒ goal( x)7. {¬p(x, y),¬p(y,coe), goal(x)} 5,68. {¬p(bob,coe), goal(art)} 1,79. {goal(art)} 4,814Who Are the Grandchildren of Art?1. {p(art,bob)} p(art,bob)2. {p(art,bud)} p(art,bud)3. {p(bob,cal)} p(bob,cal)4. {p(bob,coe)} p(bob,coe)5. {¬p(x, y), ¬p(y, z), g(x, z)} p(x , y) ∧ p(y,z) ⇒ g(x, z)6. {¬g(art, z), goal(z)} g(art, z) ⇒ goal(z)7. {¬p(art, y),¬p(y,z), goal(z)} 5,68. {¬p(bob, z),goal(z)} 1,79. {¬p(bud, z), goal(z)} 2,710. {goal(cal)} 3,811. {goal(coe)} 4,8815People and their Grandchildren?1. {p(art,bob)} p(art,bob)2. {p(art,bud)} p(art,bud)3. {p(bob,cal)} p(bob,cal)4. {p(bob,coe)} p(bob,coe)5. {¬p(x, y), ¬p(y, z), g(x, z)} p(x , y) ∧ p(y, z) ⇒ g(x, z)6. {¬g(x,z),goal(x, z)} g(x, z) ⇒ goal(x, z)7. {¬p(x, y), ¬p(y, z), goal(x, z)} 5,68. {¬p(bob, z),goal(art, z)} 1, 79. {¬p(bud, z), goal(art, z)} 2,710. {goal(art,cal)} 3,811. {goal(art,coe)} 4,816Variable Length Lists!Example[a,b,c,d]Representation as Termcons(a,cons(b,cons(c,cons(d,nil))))Shorthand(a . (b . (c . (d . nil))))Shorthand[a,b,c,d]a b c d917List MembershipMembership axioms:member(u, u . x)member(u, v . y) ⇐ member(u, y)Membership Clauses:{member(u, u . x)}{member(u, v . y), ¬member(u, y)}Answer Extraction for member(w, [a, b, c]){¬member(w, a.b.c. nil),goal(w)}{goal(a)}{¬member(w, b.c. nil)}{goal(b)}18List ConcatenationConcatenation Axioms:append(nil,y,y)append(w. x, y, w.z) ⇐ append(x, y, z)Concatenation Clauses:{append(nil,y,y)}{append(w. x, y, w.z), ¬append(x, y, z)}Answer Extraction for append([a,b],[c,d],z):{¬append(a.b.nil, c.d.nil, z), goal(z)}{¬append(b.nil, c.d.nil, z1), goal(a.z1)}{¬append(nil, c.d.nil, z2), goal(a.b.z2)}{goal(a.b.c.d.nil)}1019List ReversalReversal Example:reverse([a,b,c,d], [d,c,b,a])Reversal Axioms:reverse(x, y) ⇐ reverse2(x, nil, y)reverse2(nil, y, y)reverse2(w.x, y, z) ⇐ reverse2(x, w.y, z)Answer Extraction for reverse([a,b,c,d],z):{¬reverse(a.b.c.d.nil, z), goal(z)} …{goal(d.c.b.a.nil)}20Natural Language ProcessingGrammar:S → NP VPNP → NounNP → Noun and NounVP → Verb NPNoun → Harry | Ralph | MaryVerb → hate | hatesLogical Form: S(z) ⇐ NP(x) ∧ VP(y) ∧ append(x,y,z) NP(z) ⇐ Noun(z) NP(z) ⇐ NP(x) ∧ NP(y) ∧ append(x,and,x1) ∧ append(x1,y,z) VP(z) ⇐ Verb(x) ∧ NP(y) ∧ append(x,and,x1) ∧ append(x1,y,z) Noun(Harry) ∧ Noun(Ralph) ∧ Noun(Mary) Verb(hate) ∧ Verb(hates)1121Sentence Generation as Answer Extraction{¬S(z),goal(z)}{¬NP(x),¬VP(y),¬append(x,y,z),goal(z)}{¬VP(y),¬append(Harry,y,z),goal(z)}{¬Verb(y1),¬NP(y2),¬append(y1,y2,y),¬append(Harry,y,z),goal(z)}{¬NP(y2),¬append(hates,y2,y),¬append(Harry,y,z),goal(z)}{¬Noun(y2),¬append(hates,y2,y),¬append(Harry,y,z),goal(z)}{¬append(hates,Mary,y),¬append(Harry,y,z),goal(z)}{¬append(Harry,hates Mary,z),goal(z)}{goal(Harry hates Mary)}{goal(Harry and Ralph hate Mary)}{goal(Harry hate Mary)}{goal(Harry and Ralph hates Mary)}How can we enforce subject-verb number agreement?22Map Coloring ProblemColor the map with the 4 colors red, green,
View Full Document
Unlocking...