1Herbrand MethodComputational Logic Lecture 7Michael Genesereth Autumn 20042Propositional Interpretationspqr0 0 00 0 10 1 00 0 11 0 01 0 11 1 01 1 1For a language with n constants, there are 2ninterpretations.23Relational 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 premise also satisfies 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.35Good NewsGiven any set of sentences, there is a specially defined 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.47Herbrand InterpretationA Herbrand interpretation for a function-free language is an interpretation in which (1) the universe of discourse is theHerbrand universe for the language and (2) each object constant maps to itself.|i|={a,b}i(a) = ai(b) = bi(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}59Herbrand 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 value assigned to every object constant is itself.The interpretation for relation constant ρis the set of all tuplesof object constants τ1 ,…, τnsuch 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) = ai(b) = bi(r) = {a,b, b,b}611ExampleInterpretation|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) = ai(b) = bi(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 a set of quantifier-free sentences is satisfiable, then there is a model that satisfies it. Take the intersection of this model with the Herbrand base. By definition, this is a Herbrand model. Moreover, it is easy to see that 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.If there is no object constant, then create a tautology involving a new constant (say a) and add to the set. This does not change the satisfiability of the sentences but satisfies proof above. QED713Herbrand 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, 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: Since there are only finitely many Herbrand interpretations, the process halts.14Special Cases Ground Relational Logicno variables, no functions, no quantifiersUniversal Relational Logicno functions, no quantifiersfree variables implicitly universally quantifiedExistential Relational Logicno functionsFunctional Relational Logicno quantifiers815ExamplePremises: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 CasesGround Relational Logicno variables, no functions, no quantifiers Universal Relational Logicno functions, no quantifiersfree variables implicitly universally quantifiedExistential Relational Logicno functionsFunctional Relational Logicno quantifiers917ExamplePremises:p(x) q(x)p(a) ∨ q(a)Conclusion:q(a)Satisfaction Set:p(x) q(x)p(a) ∨ q(a)¬q(a)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}18ProblemPremisesp(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.1019Universal and Existential SentencesThe negation of a sentence ϕ in Universal Logic is the universally quantified sentence ¬∀x1...∀xn.ϕ, where x1,…, xnare the free
View Full Document
Unlocking...