Herbrand MethodPropositional InterpretationsRelational InterpretationsLogical EntailmentGood NewsHHHHerbrandHerbrand InterpretationHerbrand InterpretationsHerbrand TheoremExampleSlide 11Slide 12Basic Herbrand MethodSpecial CasesSlide 15Slide 16Slide 17ProblemUniversal and Existential SentencesSkolemizationSignificanceModified Herbrand MethodSlide 23Slide 24Slide 25Slide 26Herbrand Theorem Does Not ApplyGood News (Sort of…)Slide 29Herbrand Universe for Functional LogicHerbrand Theorem for Functional LogicSad TheoremGeneral ProblemSummaryHerbrand MethodComputational Logic Lecture 7Michael Genesereth Autumn 20072Propositional 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.3Relational Interpretations |i| a b r{,} {}{,} {}{,} {}{,} {, }{,} {}{,} {}{,} {}{,} {, }{,} {}{,} {}{,} {}{,} {, } . . .Infinitely many interpretations.4Logical EntailmentA set of premises logically entails a conclusion if and only if every interpretation that satisfies the premises also satisfies the conclusion.In the case of Propositional Logic, the number of interpretations is finite, and so it is possible to check logical entailment directly in finite time. In the case of Relational Logic, the number of interpretations is infinite, and so a direct check of logical entailment is not feasible.5Good NewsGiven any set of sentences, there is a special subset of interpretations called Herbrand interpretations.Under certain conditions, checking just the Herbrand interpretations suffices to determine logical entailment.Since there are fewer Herbrand interpretations than interpretations in general, checking just the Herbrand interpretations is less work than checking all interpretations.6HHHHerbrandThe Herbrand universe for a set of sentences in Relational Logic (with at least one object constant) is the set of all ground terms that can be formed from just the constants used in those sentences. If there are no object constants, then we add an arbitrary object constant, say a.The Herbrand base for a set of sentences is the set of all ground atomic sentences that can be formed using just the constants in the Herbrand universe.7Herbrand InterpretationA Herbrand interpretation for a function-free language is an interpretation in which (1) the universe of discourse is the Herbrand universe for the language and (2) each object constant maps to itself. |i|={a,b} i(a) = a i(b) = b i(r) = {a,a, a,b}8Herbrand Interpretations |i| a b r{a,b} a b {}{a,b} a b {a,a}{a,b} a b {a,b}{a,b} a b {b,a}{a,b} a b {b,b}{a,b} a b {a,a, a,b}{a,b} a b {a,a, b,a}{a,b} a b {a,a, b,b}{a,b} a b {a,b, b,a}{a,b} a b {a,b, b,b}{a,b} a b {b,a, b,b}{a,b} a b {a,a, a,b, b,a}{a,b} a b {a,a, a,b, b,b}{a,b} a b {a,a, b,a, b,b}{a,b} a b {a,b, b,a, b,b}{a,b} a b {a,a, a,b, b,a, b,b}9Herbrand TheoremHerbrand Theorem: A set of quantifier-free sentences in Relational Logic is satisfiable if and only if it has a Herbrand model.Construction of Herbrand model h given i.The model assigns every object constant to itself.The interpretation for relation constant is the set of all tuples of object constants 1 ,…, n such that i satisfies the sentence (1 ,…, n).10ExampleInterpretation |i|={, } i(a) = i(b) = i(r) = {,, ,}Herbrand Base {r(a,a), r(a,b), r(b,a), r(b,b)}Herbrand Interpretation |i|={a,b} i(a) = a i(b) = b i(r) = {a,b, b,b}11ExampleInterpretation |i|={, , } i(a) = i(b) = i(r) = {,, ,, ,}Herbrand Base{r(a,a), r(a,b), r(b,a), r(b,b)}Herbrand Interpretation |i|={a,b} i(a) = a i(b) = b i(r) = {a,b, b,b}12Herbrand TheoremHerbrand Theorem: A set of quantifier-free sentences is satisfiable 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 not, then create a tautology involving a constant (say a) and add to the set. This does not change the satisfiability of the sentences.If a set of quantifier-free sentences is satisfiable, then there is an interpretation that satisfies it. Take the set of all ground atoms satisfied by this interpretation. By definition, this is a Herbrand interpretation. Moreover, it satisfies the sentences. If the sentences are ground, it must agree with the original interpretation on all of the sentences, since they are all ground and mention only the constants common to both interpretations. If the sentences contain variables, the instances must all be true, including those in which the variables are replaced only by elements in the Herbrand universe. QED13Basic Herbrand MethodDefinition: Add negation of conclusion to the premises to form the satisfaction set. Loop over Herbrand interpretations. Cross out each interpretation that does not satisfy the sentences in the satisfaction set. If all Herbrand interpretations are crossed out, then, by the Herbrand Theorem, the set is unsatisfiable.Sound and Complete: Negating the conclusion leads to a contradiction; therefore, the premises logically entail the conclusion.Termination: If there are only finitely many Herbrand interpretations, the process halts.14Special 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 quantifiers15ExamplePremises:Conclusion:Satisfaction Set:p(a)⇒ q(a)p(b) ⇒ q(b)p(a)∨ p(b)q(a)∨q(b)p(a)⇒ q(a)p(b) ⇒ q(b)p(a)∨ p(b)¬(q(a)∨q(b)) p q{} {}{} {a}{} {b}{} {a,b}{a} {}{a} {a}{a} {b}{a} {a,b}{b} {}{b} {a}{b} {b}{b} {a,b}{a,b} {}{a,b} {a}{a,b} {b}{a,b} {a,b}16Special Cases Ground Relational Logicno variables, no functions, no quantifiers Universal Relational Logicno functions,
View Full Document
Unlocking...