DOC PREVIEW
Stanford CS 157 - Resolution Preliminaries

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1Resolution PreliminariesComputational Logic Lecture 9Michael Genesereth Spring 20052Resolution PrincipleThe Resolution Principle is a rule of inference.Using the Resolution Principle alone (without axiom schemataor other rules of inference), it is possible to build a theoremprover that is sound and complete for all of Relational Logic.The search space using the Resolution Principle is muchsmaller than with standard axiom schemata.23PlanFirst Lecture:UnificationRelational Clausal FormSecond Lecture:Resolution PrincipleResolution Theorem ProvingThird Lecture:True or False QuestionsFill in the Blank QuestionsResidueFourth Lecture:Strategies to enhance efficiency4Clausal FormRelational resolution works only on expressions inclausal form.Fortunately, it is possible to convert any set ofRelational Logic sentences into an equally satisfiableset of sentences in clausal form.35Clausal FormA literal is either an atomic sentence or a negation ofan atomic sentence.A clausal sentence is either a literal or a disjunction ofliterals.A clause is a set of literals (interpreted as disjunction).!{p(a)}{¬p(a)}{p(a), q(b)}The empty clause {} is unsatisfiable.6Inseadoϕ1⇒ϕ2→ ¬ϕ1∨ϕ2ϕ1⇐ϕ2→ϕ1∨ ¬ϕ2ϕ1⇔ϕ2→ (¬ϕ1∨ϕ2) ∧ (ϕ1∨ ¬ϕ2)¬¬ϕ→ϕ¬(ϕ1∧ϕ2) → ¬ϕ1∨ ¬ϕ2¬(ϕ1∨ϕ2) → ¬ϕ1∧ ¬ϕ2¬∀ν.ϕ→ ∃ν.¬ϕ¬∃ν.ϕ→ ∀ν.¬ϕImplications Out:Negations In:47Inseado (concluded)∀x. p(x) ∨ ∀x.q(x) → ∀x.p(x) ∨ ∀y.q(y)Standardize variablesExistentials Out (Outside in)∃x. p(x) → p(a)∀x.( p(x) ∧ ∃z.q(x, y, z )) → ∀x.( p(x) ∧ q(x, y, f (x, y)))8Inseado (concluded)Alls OutDistribution∀x.( p(x) ∧ q(x, y, f (x, y))) → p(x) ∧ q(x, y, f (x, y))ϕ1∨ (ϕ2∧ϕ3) → (ϕ1∨ϕ2) ∧ (ϕ1∨ϕ3)(ϕ1∧ϕ2) ∨ϕ3→ (ϕ1∨ϕ3) ∧ (ϕ2∨ϕ3)59Inseado (continued)Operators Outϕ1∧... ∧ϕn→ϕ1...ϕnϕ1∨ ... ∨ϕn→ {ϕ1,...,ϕn}10Example∃y.( g(y) ∧ ∀z.( r(z) ⇒ f (y, z)))I ∃y.( g(y) ∧ ∀z.( ¬r(z) ∨ f (y, z)))N ∃y.( g(y) ∧ ∀z.(¬r(z) ∨ f (y, z)))S ∃y.( g(y) ∧ ∀z.( ¬r(z) ∨ f (y, z)))E g(greg) ∧ ∀z.( ¬r(z) ∨ f (greg, z)))A g(greg) ∧ (¬r(z) ∨ f (greg, z)))D g(greg) ∧ (¬r(z) ∨ f (greg, z)))O {g(greg)}{¬r(z), f (greg, z)}611Example¬∃y.( g(y) ∧ ∀z.(r(z) ⇒ f (y, z)))I ¬∃y.( g(y) ∧ ∀z.(¬r(z) ∨ f (y, z)))N ¬∃y.( g(y) ∧ ∀z.(¬r(z) ∨ f (y, z)))∀y.¬(g(y) ∧ ∀z.( ¬r(z) ∨ f (y, z)))∀y.( ¬g(y) ∨ ¬∀z.(¬r(z) ∨ f (y, z)))∀y.( ¬g(y) ∨ ∃z.¬(¬r(z) ∨ f (y, z)))∀y.( ¬g(y) ∨ ∃z.( ¬¬r(z) ∧ ¬f (y, z)))∀y.( ¬g(y) ∨ ∃z.( r(z) ∧ ¬f (y, z)))S ∀y.( ¬g(y) ∨ ∃z.( r(z) ∧ ¬f (y, z)))12Example (concluded)€ ∀y.(¬g(y)∨ ∃z.(r(z)∧¬f (y,z)))E ∀y.(¬g(y)∨ (r(h(y))∧¬f (y,h(y))))A ¬g(y)∨ (r(h(y))∧¬f (y,h(y)))D (¬g(y)∨ r(h(y)))∧(¬g(y)∨¬f (y,h(y)))O {¬g (y)∨ r(h(y))}{¬g (y)∨¬f (y,h(y))}713Clausal FormBad News: The result of converting a set ofsentences is not necessarily logically equivalent tothe original set of sentences. Why? Introduction ofSkolem constants and functions.Good News: The result of converting a set ofsentences is satisfiable if and only if the original setof sentences is satisfiable. Important because we usesatisfiability to determine logical entailment.14Difficulty with Universal Instantiation€ ∀x.p(x,b)∀y.¬p(a, y)p(a,b)¬p(a,b)815SubstititionsA substitution is a finite set of pairs of variables andterms, called replacements.{X←a, Y←f(b), V←W}The result of applying a substitution σ to anexpression ϕ is the expression ϕσ obtained from ϕ byreplacing every occurrence of every variable in thesubstitution by its replacement.p(X,X,Y,Z){X←a,Y←f(b),V←W}=p(a,a,f(b),Z)16Cascaded Substitutionsr{x,y,z}{x←a, y←f(u), z←v}=r{a,f(u),v}r{a,f(u),v}{u←d, v←e}=r(a,f(d),e)r{x,y,z}{x←a,y←f(d),z←e}=r(a,f(d),e)917Composition of SubstitutionsThe composition of substitution σ and τ is thesubstitution (written compose(σ,τ) or, more simply,στ) obtained by(1) applying τ to the replacements in σ(2) adding to σ pairs from τ with different variables(3) deleting any assignments of a variable to itself.{x←a, y←f(u), z←v}{u←d,v←e,z←g}={x←a,y←f(d),z←e}{u←d,v←e,z←g}={x←a,y←f(d),z←e,u←d,v←e}18UnificationA substitution σ is a unifier for an expression ϕ andan expression ψ if and only if ϕσ=ψσ.p(X,Y){X←a,Y←b,V←b}=p(a,b)p(a,V){X←a,Y←b,V←b}=p(a,b)If two expressions have a unifier, they are said to beunifiable. Otherwise, they are nonunifiable.p(X,X)p(a,b)1019Non-Uniqueness of UnificationUnifier 1:p(X,Y){X←a,Y←b,V←b}=p(a,b)p(a,V){X←a,Y←b,V←b}=p(a,b)Unifier 2:p(X,Y){X←a,Y←f(W),V←f(W)}=p(a,f(W))p(a,V){X←a,Y←f(W),V←f(W)}=p(a,f(W))Unifier 3:p(X,Y){X←a,Y←V}=p(a,V)p(a,V){X←a,Y←V}=p(a,V)20Most General UnifierA substitution σ is a most general unifier (mgu) of twoexpressions if and only if it is as general as or moregeneral than any other unifier.Theorem: If two expressions are unifiable, then theyhave an mgu that is unique up to variable permutation.p(X,Y){X←a,Y←V}=p(a,V)p(a,V){X←a,Y←V}=p(a,V)p(X,Y){X←a,V←Y}=p(a,Y)p(a,V){X←a,V←Y}=p(a,Y)1121Expression StructureEach expression is treated as a sequence of itsimmediate subexpressions.Linear Version:p(a, f(b, c), d)Structured Version: car cdrp a df b c22Most General Unificationfunction mgu (x, y, s) {if x = y then s else if varp(x) then mguvar(x, y, s) else if atom(x) then {if varp(y) then mguvar(y, x, s) else if atom(y) then if x = y then s} else if varp(y) then mguvar(y, x, s) else if atom(y) then false else if s←mgu(car(x),car(y), s) then mgu(cdr(x), cdr(y), s)}function mguvar (x, y, s) {var dum; if dum ← assoc(x, s) then mgu(right(dum), y, s) else compose(s,{x ← plug(y,s)})}1223ExampleCall: mgu(p(X,b), p(a,Y), {}) Call: mgu(p, p, {}) Exit: {} Call: mgu(X, a, {}) Exit: {X←a} Call: mgu(b, Y, {X←a}) Exit: {X←a,Y←b}Exit: {X←a,Y←b}24ExampleCall: mgu(p(X,X), p(a,b), {}) Call: mgu(p, p, {}) Exit: {} Call: mgu(X, a, {}) Exit: {X←a} Call: mgu(X, b, {X←a}) Call: mgu(a, b, {X←a}) Exit: false Exit: falseExit: false1325ExampleCall: mgu(p(f(X),f(X)), p(Y,f(a)), {}) Call: mgu(p, p, {}) Exit: {} Call: mgu(f(X), Y, {}) Exit: {Y←f(X)} Call: mgu(f(X), f(a), {Y←f(X)}) Call: mgu(f, f, {Y←f(X)}) Exit: {Y←f(X)} Call: mgu(X, a, {Y←f(X)}) Exit: {Y←f(a),X←a}


View Full Document

Stanford CS 157 - Resolution Preliminaries

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 Resolution Preliminaries
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 Resolution Preliminaries 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 Resolution Preliminaries 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?