EqualityCoreferentialitySlide 3ExampleUnique Names AssumptionDomain Closure AssumptionHerbrandIncompletenessTwo ApproachesEquality AxiomsEquality Axioms in Rule FormEquality ProofEquality ProblemFlatteningProof With FlatteningSubstitution AxiomProof With Substitution AxiomNotesSlide 19Motivation for DemodulationDemodulationExamplesNon-ExamplesParent DeletionProof With DemodulationSlide 26Slide 27Problems With DemodulationParamodulationDifferencesSlide 31Proof With ParamodulationSlide 33PowerEqualityComputational Logic Lecture 15Michael Genesereth Autumn 20072CoreferentialityDifferent terms can sometimes refer to the same object.2+2 2*2 4In some situations, we want to say explicitly that two terms are coreferential; and, in some 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 distinct name refers to a distinct object, i.e. every object has at most one name. This is called the unique names assumption (UNA). The upshot is that a difference in name implies a difference in referent.= if and only if i = iThe unique names assumption is not true in general!!!Question: How does one express the unique names assumption in Relational Logic?6Domain Closure AssumptionIn many applications, one makes the assumption that all objects are named, i.e. every object has at least one name. This is called the domain closure assumption (DCA).The domain closure assumption is not true in general!!!Question: How does one express the domain closure assumption in Relational Logic?7HerbrandThe 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?8IncompletenessTheorem: 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? Goal9Two ApproachesAxiomatic approach -- add axioms of equalityProof Theoretic approach -- add new rules of inference10Equality AxiomsReflexivityx.x=xSymmetry:x.y.(x=y y=x)Transitivity:x.y. z.(x=y y=z x=z)11Equality Axioms in Rule FormReflexivityx=xSymmetry:x=y y=xTransitivity:x=z x=y y=z12Equality 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,913Equality 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,914FlatteningEquivalence: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?15Proof 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,716Substitution AxiomFlattening Rule:f(f(a))=a x.(f(a)=x f(x)=a)Substitution Axiom:f(x)=z x=y f(y)=z17Proof With Substitution Axiom€ 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,918NotesSubstitution 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.19Two ApproachesAxiomatic approach -- add axioms of equalityProof Theoretic approach -- add new rules of inference20Motivation for Demodulation€ p(a, f (b,g(a,h(b)),c),d)b = ep(a, f (e,g(a,h(e)),c),d)21Demodulation{ϕ1,...,ϕn}{τ1=τ2}{ϕ1,...,ϕn}[τ1σ ← τ2σ]where τ occurs in ϕi where τ1σ =τ22Examples€ 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)23Non-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 Only24Parent 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.25Proof 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,526Proof 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,1227Proof 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,628Problems 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 =
View Full Document
Unlocking...