1Relational ProofsComputational Logic Lecture 8Michael Genesereth Spring 20052Logical EntailmentA set of premises logically entails a conclusion if and only ifevery interpretation that satisfies the premises also satisfies theconclusion.23Herbrand SummaryHerbrand Method works for Basic Logic and Universal Logic,but there can be many interpretations.Herbrand Method does not work for Existential Logic unlesssentences rewritten in Functional 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.35Old Rules of InferenceModus Ponens (MP) Modus Tolens (MT)And Introduction (AI) And Elimination (AE)ϕ⇒ψϕψϕ⇒ψ¬ψ¬ϕϕ∧ψϕψϕψϕ∧ψ6Idea for Universal Instantiation∀ν.ϕϕ[ν←τ]Warning: This is not quite right.47Examples∀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) x←jane∃y.hates(y,y) x←y Wrong!!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).59SubstitutabilityA 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 ϕ611Existential Instantiation I∃ν.ϕϕ[ν←σ]where ϕ contains no free variableswhere σ is a new object constant12Examples∃y.p(y)p(c)∃y.y*y=01*1=0 Wrong!∃y.y*y=xc*c=x Wrong!c*c=4c*c=6713Existential 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)=x Wrong!815Formal 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,mike) EI : 35. ∀v.∀w.(loves(v, w) ⇒ loves( jack, v)) UI : 26. ∀w.(loves( jill, w) ⇒ loves( jack, jill)) UI : 57. loves( jill,mike) ⇒ loves( jack, jill) UI : 68. loves( jack, jill) MP : 7, 4917Harry 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)1019Harry and Ralph (continued)20Standard Axiom SchemataAll generalizations* of the following:II: ϕ ⇒ (ψ ⇒ ϕ)ID: (ϕ ⇒ (ψ ⇒ χ)) ⇒ ((ϕ ⇒ ψ) ⇒ (ϕ ⇒ χ))CR: (¬ψ ⇒ ϕ) ⇒ ((¬ψ ⇒ ¬ϕ) ⇒ ψ)(ψ ⇒ ϕ) ⇒ ((ψ ⇒ ¬ϕ) ⇒ ¬ψ)EQ: (ϕ ⇔ ψ) ⇒ (ϕ ⇒ ψ)(ϕ ⇔ ψ) ⇒ (ψ ⇒ ϕ)(ϕ ⇒ ψ) ⇒ ((ψ ⇒ ϕ) ⇒ (ϕ ⇔ ψ))OQ:!! (ϕ ⇐ ψ) ⇔ (ψ ⇒ ϕ)(ϕ ∨ ψ) ⇔ (¬ϕ ⇒ ψ)(ϕ ∧ ψ) ⇔ ¬(¬ϕ ∨ ¬ψ)*A generalization of ϕ is ∀ν1...∀νk.ϕ, for variables ν1,...,νk.1121Standard Axiom Schemata (concluded)UD: ∀ν.(ϕ ⇒ ψ) ⇒ (∀ν.ϕ ⇒∀ν.ψ)UG: ϕ ⇒ ∀ν.ϕwhere ν is not free in ϕUI: ∀ν.ϕ ⇒ ϕ[ν←τ]where τ is free for ν in !ϕED: ∃ν.ϕ ⇔¬∀ν.¬ϕ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 Δ.1223DecidabilityA 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.1325Semidecidability 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 entailed either!p(x) ⇒ p(f(x))p(f(f(a)))¬p(f(b))?1427Undecidability of Logical EntailmentMetatheorem: Logical Entailment for Relational Logic is notdecidable.Proof: Suppose there is a machine p that decides the questionof logical entailment. Its inputs are Δ and ϕ.We can encode the behavior of this 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 also 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Δ1529ClosureThe 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)
View Full Document
Unlocking...