EqualityCoreferentialitySlide 3ExampleUnique Names AssumptionHerbrandIncompletenessTwo ApproachesEquality AxiomsEquality Axioms in Rule FormEquality ProofEquality ProblemFlatteningProof With FlatteningSubstitution AxiomProof With SubstitutionNotesMotivation for DemodulationDemodulationExamplesNon-ExamplesParent DeletionProof With DemodulationSlide 24Slide 25Problems With DemodulationParamodulationDifferencesSlide 29Proof With ParamodulationSlide 31PowerEqualityComputational Logic Lecture 16Michael Genesereth Spring 20052CoreferentialityDifferent terms can sometimes refer to the same object.2+2 2*2 4In many situations, we want to say explicitly that two terms are coreferential; and, in many situations, we want to say explicitly that two terms are not coreferential. For this, we use equality.2+22*22+22*3Coreferentiality3EqualityAn equation = is true in an interpretation i if and only if the terms in the equation refer to the same object in the universe of discourse.i = i4ExampleInterpretation: i(a) = i(b) = i(c) = i(f ) = {, } i(r) = {, , , }Satisfied Sentences a = a a = f(b) a= f(f(a)) a b b = f(a) a=f(f(c)) a = c b = f(c) b=f(f(b)) b = b c = f(b) c=f(f(a)) b c c=f(f(c))5Unique Names AssumptionIn many applications, one makes the assumption that every object has a unique name. This is called the unique names assumption (UNA). The upshot is that a difference in name implies a difference in referent.= i = iThe unique names assumption is not true in general!!!Question: How does one express the unique names assumption in Relational Logic?6HerbrandThe Herbrand Theorem does not hold in the presence of equality. In general, different constants may refer to the same object. In a Herbrand interpretation, every constant refers to itself. Thus, the following sentence is satisfiable, but there is no Herbrand interpretation that satisfies it.john=jackQuestion: Does the Herbrand theorem hold in the presence of the unique names assumption?7IncompletenessTheorem: Resolution (with factoring) is refutation complete for Relational Logic*.*without equality.Theorem: There is a set of premises and a conclusion (involving equality) such that logically implies but cannot be proved from using Resolution.1. b=a Premise2. b=c Premise3. a=c? Goal8Two ApproachesAxiomatic approach -- add axioms of equalityProof Theoretic approach -- add new rules of inference9Equality AxiomsReflexivityx.x=xSymmetry:x.y.(x=y y=x)Transitivity:x.y.z.(x=y y=z x=z)10Equality Axioms in Rule FormReflexivityx=xSymmetry:x=y y=xTransitivity:x=z x=y y=z11Equality Proof€ 1. b = a Premise2. b = c Premise3. x = x Equality4. x = y ⇐ y = x Equality5. x = z ⇐ x = y ∧y = z Equality6. a = c? Goal7. a = y ∧y = c? 5,68. y = a ∧y = c? 4,79. b = c? 1,810. ? 2,912Equality Problem€ 1. f (a) = b Premise2. f (b) = a Premise3. x = x Equality4. x = y ⇐ y = x Equality5. x = z ⇐ x = y ∧y = z Equality6. f ( f (a)) = a? Goal7. a = f ( f (a))? 4,68. f ( f (a)) = y ∧y = a? 5,69. f ( f (a)) = w ∧w = y ∧y = a? 5,810. f ( f (a)) = v ∧v = w ∧w = y ∧y = a? 5,913FlatteningEquivalence:f(f(a))=a x.(f(a)=x f(x)=a)Rewrite: f(f(a))=aAs: x.(f(a)=x f(x)=a)As: f(a)=c f(c)=aAs: f(a)=c f(c)=aRewrite: f(f(a))=a?As: x.(f(a)=x f(x)=a)?As: f(a)=x f(x)=a?14Proof With Flattening€ 1. f (a) = b Premise2. f (b) = a Premise3. x = x Equality4. x = y ⇐ y = x Equality5. x = z ⇐ x = y ∧y = z Equality6. f (a) = x ∧ f (x) = a? f ( f (a)) = a?7. f (b) = a? 1,68. ? 2,715Substitution AxiomFlattening Rule:f(f(a))=a x.(f(a)=x f(x)=a)Substitution Axiom:f(x)=z x=y f(y)=z16Proof With Substitution€ 1. f (a) = b Premise2. f (b) = a Premise3. x = x Equality4. x = y ⇐ y = x Equality5. x = z ⇐ x = y ∧y = z Equality6. f (x) = z ⇐ x = y ∧ f (y) = z? Substitution7. f ( f (a)) = a? Goal8. f (a) = y ∧ f (y) = a? 6, 79. f (b) = a? 1,810. ? 2,917NotesSubstitution axioms for relation constants too.p(x) x=y p(y)Substitution axioms for multiple argumentsp(x,y)=z x=u y=v p(u,v)Need one substitution for each function and relation constant.18Motivation for Demodulation€ p(a, f (b,g(a,h(b)),c),d)b = ep(a, f (e,g(a,h(e)),c),d)19Demodulation{ϕ1,...,ϕn}{τ1=τ2}{ϕ1,...,ϕn}[τ1σ ← τ2σ]where τ occurs in ϕi where τ1σ =τ20Examples€ p(a, f (b,g(a,h(b)),c),d)b = ep(a, f (e,g(a,h(e)),c),d)€ p(a, f (b,g(a,h(b)),c),d)g(x, y) = j(x)p(a, f (b, j(a),c),d)21Non-Examples€ p(a, g(a,b),c)g(a, y) = y ⇐ p(y)p(a, g(a,b),c) ⇐ p(b)€ p(a, g(x,b),c)g(a, y) = j(y)p(a, j(b),c)Unit Equations OnlyVariables Substituted in Equation Only22Parent Deletion1. a =1 a=12. p(a,a,a) p(a,a,a)3. p(a,a,1) p(a,a,1)4. p(a,1,1) p(a,1,a)5. p(1,1,1) p(a,1,1)6. p(1,a,a)7. p(1,a,1)8. p(1,1,a)9. p(1,1,1)In Demodulation, parent is usually deleted after substitution.23Proof With Demodulation€ 1. f (a) = b Premise2. f (b) = a Premise3. x = x Equality4. f ( f (a)) = a? Goal5. f (b) = a? 1,46. ? 2,524Proof With Demodulation1. f(1) =1 Premise2. f(x) =x* f(x−1) Premise3. x=x Equality4. arithmeticaxioms Premise5. f(3) =z? Goal6. 3* f(3−1) =z? 2,57. 3* f(2) =z? 4,68. 3* 2* f(2−1) =z? 2,79. 3* 2* f(1) =z? 4,810. 3* 2*1=z? 1,911. 3* 2=z? 4,1012. 6=z? 4,1113. ? 3,1225Proof With DemodulationSuppose Bill is Joe's paternal grandfather and suppose that Bill is kind. Prove that Joe's paternal grandfather is kind.€ 1. pgf ( joe) = bill Premise2. f ( f (x)) = pgf (x) Premise3. kind(bill) Premise4. kind( f ( f ( joe)))? Goal5. kind(pgf ( joe))? 2,46. kind(bill)? 1,57. ? 3,626Problems With DemodulationCannot bind variables in expression:€ father(pat) = quincyolder( father(x), x)older(quincy, pat)Equation must be a unit clause€ father(x) = y ⇐ x = pat ∧y = quincyolder( father(x), x)older(quincy, pat) ⇐ x = pat ∧y = quincy27Paramodulation€ {ϕ1,...,ϕn}{ψ1,...,τ1= τ2,...,ψn}{ϕ1,...,ϕn,ψ1,...,ψn}σ[τ1σ ← τ2σ ]where τ occurs in ϕi where τ1σ = τσ28Differences(1) Demodulation requires a unit equation.(2) Demodulation binds variables in equation only.(3) Demodulation deletes parent.29Example€ {p( f (x,b), x),q(x)}{ f (a, y) = y,r(y)}{p(b,a),q(a),r(b)}30Proof With Paramodulation€ 1. { father(pat) = quincy} Premise2. {older( father(x), x)} Premise3. {¬ older(quincy, pat)} Goal4.
View Full Document
Unlocking...