Relational ProofsComputational LogicLecture 8Michael GeneserethSpring 20022Logical EntailmentA set of premises logically entails a conclusion if and only ifevery interpretation that satisfies the premises also satisfies theconclusion.3Herbrand SummaryHerbrand Method works for Basic Logic and Universal Logic,but there can be many interpretations.Herbrand Method does not work for Existential Logic.Herbrand Method works for Functional Logic, but infinitelymany interpretationsSolution: Use formal proofs!4Formal ProofsA formal proof of ϕ from ∆ is a sequence of sentencesterminating in ϕ in which each item is either:1. a premise (a member of ∆)2. an instance of an axiom schema3. the result of applying a rule of inference to earlier itemsin the sequence.5Old Rules of InferenceModus Ponens (MP)Modus Tolens (MT)And Introduction (AI)And Elimination (AE)ϕ ⇒ψϕψϕ ⇒ψ¬ψ¬ϕϕ ∧ψϕψϕψϕ ∧ψ6Idea for Universal Instantiation∀ν.ϕϕ[ν ←τ]Warning: This is not quite right.7Examples∀y.hates(jane,y)hates(jane,jill) y←jillhates(jane,mother(jane)) y←mother(jane)hates(jane,y) y←yhates(jane,z) y←z∀x.∃y.hates(x,y)∃y.hates(jane,y) y←jane∃y.hates(y,y) y←yWrong!!8InappropriatenessA term τ is inappropriate for a variable ν in ϕ if and only if τcontains a variable µ and there is some free occurrence of ν inϕ that lies in the scope of a quantifier of µ.mother(x) is inappropriate for y in ∃x.hates(x,y).9SubstitutabilityA term τ is substitutable for ν in ϕ if and only if it is notinappropriate with ν in ϕ.Some texts say “x is free for y in ϕ” instead of “x issubstitutable for y in ϕ”.mother(jane) is free for y in hates(jane,y).mother(x) is free for y in hates(jane,y).mother(x) is free for y in ∃z.hates(z,y).mother(x) is not free for y in ∃x.hates(x,y).mother(x) is free for y in (∀x.∀y.loves(x,y) ∧ ∃z.hates(z,y)).10Universal Instantiation∀ν.ϕϕ[ν ←τ]where τ is free for ν in ϕ11Existential Instantiation I∃ν.ϕϕ[ν ←σ]where ϕ contains no free variableswhere σ is a new object constant12Examples∃y.p(y)p(c)∃y.y*y=01*1=0Wrong!∃y.y*y=xc*c=xWrong!c*c=4c*c=613Existential Instantiation II∃ν.ϕϕ[ν ← π(τ1,...,τn)]where τ1,...,τn are free in ϕwhere π is a new function constant14Examples∃y.y*y=xf(x)*f(x)=xf(4)*f(4)=4f(6)*f(6)=6∃y.y*y=xsqrt(x)*sqrt(x)=xlog(x)*log(x)=xWrong!15Formal ProofsA formal proof of ϕ from ∆ is a sequence of sentencesterminating in ϕ in which each item is either:1. a premise (a member of ∆)2. an instance of an axiom schema3. the result of applying a rule of inference to earlier itemsin the sequence.16ExampleEverybody loves somebody. Everybody loves a lover. Showthat Jack loves Jill.1. ∀x.∃y.loves(x, y)Premise2. ∀u.∀v.∀w.(loves(v,w) ⇒ loves(u,v))Premise3. ∃y.loves(jill,y)UI:14. loves(jill, f (jill)) EI :35. ∀v.∀w.(loves(v,w) ⇒ loves(jack,v))UI: 26. ∀w.(loves(jill,w) ⇒ loves(jack,jill))UI: 57. loves(jill, f (jill)) ⇒ loves(jack,jill)UI: 68. loves(jack,jill) MP :7,417Harry and RalphEvery horse can outrun every dog. Some greyhounds canoutrun every rabbit. Harry is a horse. Ralph is a rabbit. CanHarry outrun Ralph?18Harry and Ralph (continued)19Harry and Ralph (continued)20Standard Axiom SchemataAll generalizations* of the following:II: ϕ ⇒ (ψ ⇒ ϕ)ID:(ϕ ⇒ (ψ ⇒ χ)) ⇒ ((ϕ ⇒ ψ) ⇒ (ϕ ⇒ χ))CR: (¬ψ ⇒ ϕ) ⇒ ((¬ψ ⇒ ¬ϕ) ⇒ ψ)(ψ ⇒ ϕ) ⇒ ((ψ ⇒ ¬ϕ) ⇒ ¬ψ)EQ: (ϕ ⇔ ψ) ⇒ (ϕ ⇒ ψ)(ϕ ⇔ ψ) ⇒ (ψ ⇒ ϕ)(ϕ ⇒ ψ) ⇒ ((ψ ⇒ ϕ) ⇒ (ϕ ⇔ ψ))OQ: (ϕ ⇐ ψ) ⇔ (ψ ⇒ ϕ)(ϕ ∨ ψ) ⇔ (¬ϕ ⇒ ψ)(ϕ ∧ ψ) ⇔ ¬(¬ϕ ∨ ¬ψ)21Standard Axiom Schemata (continued)UD:∀ν.(ϕ ⇒ ψ) ⇒ (∀ν.ϕ ⇒∀ν.ψ)UG:ϕ ⇒ ∀ν.ϕwhere ν is not free in ϕUI:∀ν.ϕ ⇒ ϕ[ν←τ]where τ is free for ν in ϕED: ∃ν.ϕ ⇔¬∀ν.¬ϕ*A generalization of ϕ is ∀ν1...∀νk.ϕ, for variables ν1,...,νk.22ProvabilityA sentence ϕ is provable from a set of sentences ∆ if and onlyif there is a finite formal proof of ϕ from ∆ using only ModusPonens and the standard axiom schemata.Soundness Theorem: If ϕ is provable from ∆, then ∆ logicallyentails ϕ.Completeness Theorem (Godel): If ∆ logically entails ϕ, then ϕis provable from ∆.23DecidabilityA class of questions is decidable if and only if there is aprocedure such that, when given as input any question in theclass, the procedure halts and says yes if the answer is positiveand no if the answer is negative.Example: For any natural number n, determining whether n isprime.24SemidecidabilityA class of questions is semidecidable if and only if there is aprocedure that halts and says yes if the answer is positive.Obvious Fact: If a class of questions is decidable, it issemidecidable.25Semidecidability of Logical Entailmentproof <- kbgoal in proof?r <- choose(rules)p <- choose(proof)q <- choose(proof)c <- apply(r,p,q)proof <- proof|cSuccessgoalkbrules26Decidability Not ProvedNote that we have not shown that logical entailment forRelational Logic is decidable.The procedure may not halt.p(x) ⇒ p(f(x))p(f(f(a)))p(f(b))?We cannot just run procedure on negated sentence because thatmay not be logically implied either!p(x) ⇒ p(f(x))p(f(f(a)))¬p(f(b))?27Undecidability of Logical EntailmentMetatheorem: Logical Entailment for Relational Logic is notdecidable.Proof: Suppose there is a procedure p that decides the questionof logical entailment. Its inputs are ∆ and ϕ.We can encode the behavior of a machine and its inputs assentences and ask whether the machine halts as a conclusion.What happens if we give this description and question to p? Itsays yes.YesNopδφ28Undecidability (continued)It is possible to construct a larger machine p’ that enters aninfinite loop if p says yes and halts if p says no.We can encode a description of this machine as a set ofsentences and ask whether the machine halts as a conclusion.What happens if we give this description and question to p? Ifp says yes, then p’ runs forever, contradicting the hypothesisthat p computes correctly. If p says no, then p’ halts, onceagain contradicting answer from p. QEDNopHaltsδ29ClosureThe closure S* of a set S of sentences is the set of allsentences logically entailed by S.S*={ϕ | S|=ϕ}Set of Sentences:Closure:p(a) p(a)p(x)⇒p(f(x)) p(f(a)) p(f(f(a))) p(a) ∧ p(f(a)) p(x)⇒p(f(x))
View Full Document
Unlocking...