Herbrand MethodComputational LogicLecture 7Michael Genesereth Autumn 20022Propositional Interpretationsp q r0 0 00 0 10 1 00 0 11 0 01 0 11 1 01 1 1For a language with n constants, there are 2n interpretations.{}{r}{q}{q,r}{p}{p,r}{p,q}{p,q,r}3Relational Interpretations{}{p(a)}{q(a)}{p(a),q(a)}{p(b)}{q(b)}{p(b),q(b)}{p(a),p(b)}{p(a),p(b),q(a)}{p(a),p(b),q(b)}{p(a),p(b),q(a), q(b)}. ..Infinitely many interpretations.4Logical EntailmentA set of premises logically entails a conclusion if and only ifevery interpretation that satisfies the premise also satisfiesconclusion.In the case of Propositional Logic, the number ofinterpretations is finite, and so it is possible to check logicalentailment directly in finite time.In the case of Relational Logic, the number of interpretationsis infinite, and so a direct check of logical entailment is notfeasible.5Good NewsGiven any set of sentences, there is a specially definedsubset of interpretations called Herbrand interpretations.Under certain conditions, checking just the Herbrandinterpretations suffices to determine logical entailment.Checking just the Herbrand interpretations is less work thanchecking all interpretations.6HHHHerbrandThe Herbrand universe for a set of sentences in RelationalLogic (with at least one object constant) is the set of all groundterms that can be formed from just the constants used in thosesentences. If there are no object constants, then we add anarbitrary object constant, say a.The Herbrand base for a set of sentences is the set of allground atomic sentences that can be formed using just theconstants in the Herbrand universe.A Herbrand model for a set of sentences is any subset of theHerbrand base for those sentences.7ExampleSentences∀x.(r(a,x) ⇒ r(x,b))∀x.∀y.∀z.(r(x,y) ∧r(x,y) ⇒ r(x,z))Herbrand Universe (constants used in sentences only){a,b}Herbrand Base{r(a,a), r(a,b), r(b,a), r(b,b)}8Herbrand Interpretations{}{r(a,a)}{r(a,b)}{r(b,a)}{r(b,b)}{r(a,a), r(a,b)}{r(a,a), r(b,a)}{r(a,a), r(b,b)}{r(a,b), r(b,a)}{r(a,b), r(b,b)}{r(b,a), r(b,b)}{r(a,a), r(a,b), r(b,a)}{r(a,a), r(a,b), r(b,b)}{r(a,a), r(b,a), r(b,b)}{r(a,b), r(b,a), r(b,b)}{r(a,a), r(a,b), r(b,a), r(b,b)}16 Herbrand interpretations in all. Note: 16<∞.9Herbrand TheoremHerbrand Theorem: A set of quantifier-free sentences issatisfiable if and only if it has a Herbrand model that satisfies it.Proof. Assume the set of sentences contains at least one object constant. If aset of quantifier-free sentences is satisfiable, then there is a model thatsatisfies it. Take the intersection of this model with the Herbrand base. Bydefinition, this is a Herbrand model. Moreover, it is easy to see that itsatisfies the sentences. If the sentences are ground, it must agree with theoriginal interpretation on all of the sentences, since they are all ground andmention only the constants common to both interpretations. If the sentencescontain variables, the instances must all be true, including those in which thevariables are replaced only by elements in the Herbrand universe.If there is no object constant, then create a tautology involving a newconstant (say a) and add to the set. This does not change the satisfiability ofthe sentences but satisfies proof above. QED10ExampleSentencesr(a,b) ⇒ r(b,b)r(a,b) ∨ r(b,b)Model{r(a,b), r(b,b), r(a,c), r(b,c)}Herbrand Base{r(a,a), r(a,b), r(b,a), r(b,b)}Herbrand Model{r(a,b), r(b,b)}11ExampleSentencesr(a,x)r(x,y) ⇒ r(y,x)Model{r(a,a), r(a,b), r(a,c), r(b,a), r(c,a)}Herbrand Base{r(a,a)}Herbrand Model{r(a,a)}12Herbrand MethodDefinition: Add negation of conclusion to the premises to formthe satisfaction set. Loop over Herbrand interpretations. Crossout each interpretation that does not satisfy the sentences in thesatisfaction set. If all Herbrand interpretations are crossed out,by the Herbrand Theorem, the set is unsatisfiable.Sound and Complete: Negating the conclusion leads to acontradiction; therefore, the premises logically entail theconclusion.Termination: Since there are only finitely many Herbrandinterpretations, the process halts.13Special Cases„ Ground Relational Logicno variables, no functions, no quantifiers Universal Relational Logicno functions, no quantifiersfree variables implicitly universally quantified Existential Relational Logicno functions Functional Relational Logicno quantifiers14ExamplePremises:Conclusion:Satisfaction Set:p(a) ⇒ q(a)p(b) ⇒ q(b)p(a)∨ p(b){}{q(a)}{q(b)}{q(a),q(b)}{p(a)}{p(a), q(a)}{p( a), q(b)}{p( a), q(a),q(b)}{p( b)}{p( b), q(a)}{p( b), q(b)}{p( b), q(a),q(b)}{p( a), p(b)}{p( a), p(b),q(a)}{p( a), p(b),q(b)}{p( a), p(b),q(a),q(b)}q(a)∨ q(b)p(a) ⇒ q(a)p(b) ⇒ q(b)p(a)∨ p(b)¬(q(a)∨ q(b))15Special Cases Ground Relational Logicno variables, no functions, no quantifiers„ Universal Relational Logicno functions, no quantifiersfree variables implicitly universally quantified Existential Relational Logicno functions Functional Relational Logicno quantifiers16ExamplePremises: Herbrand Interpretations:p(x) ⇒ q(x)p(a) ∨ q(a)Conclusion:q(a)Satisfaction Set:p(x) ⇒ q(x)p(a) ∨ q(a)¬q(a){}{p(a)}{q(a)}{p(a),q(a)}17ProblemPremisesp(x) ⇒ q(x)p(x) ∨ q(x)Conclusionq(x)What is the Satisfaction set?¬q(x)No. This says q is false for all args.¬∀x.q(x)Yes, but this has an explicit quantifier.18Universal and Existential SentencesThe negation of a sentence ϕ in Universal Logic is theuniversally quantified sentence ¬∀x1...∀xn.ϕ, where x1,…, xnare the free variables in ϕ.Negation distributed over universal quantification by flippingthe universal quantifier to an existential quantifier.¬∀x1...∀xn.ϕ↓∃x1... ∃xn.¬ϕIf a sentence is purely universal, then this distribution leads toa purely existential sentence.19SkolemizationThe Skolemization of a purely existential sentence is thesentence obtained by dropping the existential quantifiers andreplacing all variables systematically by brand new constants.Example:∃x.¬q(x)↓¬q(c)Example:∃x.∃y.(p(x,y) ∧ q(x,b))↓p(c,d) ∧ q(c,b)20SignificanceSkolemization Theorem: A set of sentences in RelationalLogic is satisfiable if and only if its Skolemization issatisfiable.A modification of the Herbrand Method can be used!21Modified Herbrand MethodOriginal Definition: Add negation of conclusion to thepremises to form the satisfaction set... Loop over Herbrandinterpretations…New Definition: Negate the conclusion. Add itsSkolemization to the premises to form
View Full Document
Unlocking...