Unformatted text preview:

1ApplicationsComputational Logic Lecture 11Michael Genesereth Autumn 20062PlanFirst 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 Δ of sentenceslogically entails a closed sentence ϕ, rewrite Δ∪{¬ϕ} inclausal form and try to derive the empty clause.Alternate Method: To determine whether a set Δ of sentenceslogically entails a closed sentence ϕ , rewrite Δ∪{ϕ ⇒ goal}in clausal form and try to derive goal.Intuition: The sentence (ϕ ⇒ goal) is equivalent to thesentence (¬ϕ ∨ 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 Determining Logical Entailment: Todetermine whether a set Δ of sentences logically entails aclosed sentence ϕ , rewrite Δ∪{ϕ ⇒ goal} in clausal form andtry 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 and try to derivegoal(ν1,…,νn).Intuition: The sentence (q(z) ⇒ goal(z)) says that, whenever, zsatisfies q, it satisfies the “goal”.8ExampleGiven (p(x) ⇒ q(x)) and p(a), find a term τ such that q(τ) istrue.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 thatq(τ) 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,36. {goal(a)} 2, 57. {goal(b)} 3,510ExampleGiven (p(x) ⇒ q(x)) and (p(a) ∨ p(b)), find a term τ such thatq(τ) 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, cons(u, x))member(u, cons(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]){¬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(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)}22Map Coloring ProblemColor the map with the 4 colors red, green, blue, and


View Full Document

Stanford CS 157 - Lecture Notes

Documents in this Course
Lecture 1

Lecture 1

15 pages

Equality

Equality

32 pages

Lecture 19

Lecture 19

100 pages

Epilog

Epilog

29 pages

Equality

Equality

34 pages

Load more
Download Lecture Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?