1Resolution PreliminariesComputational Logic Lecture 9Michael Genesereth Autumn 20072Resolution PrincipleThe Resolution Principle is a rule of inference.Using the Resolution Principle alone (without axiomschemata or other rules of inference), it is possible tobuild a theorem prover that is sound and complete forall of Relational Logic.The search space using the Resolution Principle ismuch smaller than with standard axiom schemata.23PlanFirst Lecture - Resolution PreliminariesRelational Clausal FormUnificationSecond Lecture - Resolution PrincipleResolution Principle and FactoringResolution Theorem ProvingThird Lecture - Resolution Applications Theorem ProvingAnswer ExtractionReductionFourth Lecture - Resolution StrategiesElimination Strategies (tautology elimination, subsumption, …)Restriction Strategies (ancestry filtering, set of support, …)4Clausal 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(x), q(x)}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 (continued)∀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 (continued)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∨ϕn)(ϕ1∧ϕ2)∨ϕ3→ (ϕ1∨ϕ3)∧(ϕ2∨ϕ3)ϕ∨(ϕ1∨...∨ϕn) → (ϕ∨ϕ1∨...∨ϕn)(ϕ1∨...∨ϕn)∨ϕ→ (ϕ1∨...∨ϕn∨ϕ)ϕ∧(ϕ1∧...∧ϕn) → (ϕ∧ϕ1∧...∧ϕn)(ϕ1∧...∧ϕn)∧ϕ→ (ϕ1∧...∧ϕn∧ϕ)59Inseado (concluded)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:p a df b c22Most General Unification (preliminary)function mgu (x, y, s) {if (varp(x)) {return mguvar(x, y, s)}; if (atom(x)) {return mguatom(x, y, s)}; if (varp(y)) {return mguvar(y, x, s)}; if (atom(y)) {return false}; for (var i=0; i < x.length; i++) {s = mgu(x[i], y[i], s); if (s == false) {return false}}; return s}1223Most General Unification (preliminary)function mguatom (x, y, s) {if (varp(y)) {return mguvar(y, x, s)}; if (x == y) {return s}; return false}function mguvar (x, y, s) {if (x == y) {return s}; var dum = getbinding(x, s); if (dum != false) {return mgu(dum, y, s)}; return compose(s,{x ←plug(y, s)})}24ExampleCall: mgu(p(X,b), p(a,Y), {}) Call: mgu(p, p,
View Full Document
Unlocking...