Existential instantiation contd. Ul can be applied several times to add new sentences; the new KB is logically equivalent to the old El can be applied once to replace the existential sentence; the new KB is not equivalent to the old, but is satisfiable iff the old KB was satisfiable Chapter 9 6
Existential instantiation contd. UI can be applied several times to add new sentences; the new KB is logically equivalent to the old EI can be applied once to replace the existential sentence; the new KB is not equivalent to the old, but is satisfiable iff the old KB was satisfiable Chapter 9 6
Reduction to propositional inference Suppose the KB contains just the following: Vx King(x)A Greedy(x)Evil(x) King(John) Greedy(John) Brother(Richard,John) Instantiating the universal sentence in all possible ways,we have Kimg(John)∧Greedy(John)→Evil(Johm) King(Richard)A Greedy(Richard)Evil(Richard) King(John) Greedy(John) Brother(Richard,John) The new KB is propositionalized:proposition symbols are King(John),Greedy(John),Evil(John),King(Richard)etc Chapter 9 7
Reduction to propositional inference Suppose the KB contains just the following: ∀ x King(x) ∧ Greedy(x) ⇒ Evil(x) King(John) Greedy(John) Brother(Richard, John) Instantiating the universal sentence in all possible ways, we have King(John) ∧ Greedy(John) ⇒ Evil(John) King(Richard) ∧ Greedy(Richard) ⇒ Evil(Richard) King(John) Greedy(John) Brother(Richard, John) The new KB is propositionalized: proposition symbols are King(John), Greedy(John), Evil(John), King(Richard) etc. Chapter 9 7
Reduction contd. Claim:a ground sentence*is entailed by new KB iff entailed by original KB Claim:every FOL KB can be propositionalized so as to preserve entailment Idea:propositionalize KB and query,apply resolution,return result Problem:with function symbols,there are infinitely many ground terms, e.g.,Father(Father(Father(John)) Theorem:Herbrand(1930).If a sentence a is entailed by an FOL KB, it is entailed by a finite subset of the propositional KB ldea:For n=0 to oo do create a propositional KB by instantiating with depth-n terms see if a is entailed by this KB Problem:works if a is entailed,loops if a is not entailed Theorem:Turing(1936),Church(1936),entailment in FOL is semidecidable Chapter 9 8
Reduction contd. Claim: a ground sentence∗ is entailed by new KB iff entailed by original KB Claim: every FOL KB can be propositionalized so as to preserve entailment Idea: propositionalize KB and query, apply resolution, return result Problem: with function symbols, there are infinitely many ground terms, e.g., Father(Father(Father(John))) Theorem: Herbrand (1930). If a sentence α is entailed by an FOL KB, it is entailed by a finite subset of the propositional KB Idea: For n = 0 to ∞ do create a propositional KB by instantiating with depth-n terms see if α is entailed by this KB Problem: works if α is entailed, loops if α is not entailed Theorem: Turing (1936), Church (1936), entailment in FOL is semidecidable Chapter 9 8
Problems with propositionalization Propositionalization seems to generate lots of irrelevant sentences. E.g.,from Vx King(x)∧Greedy(x)→Evil(c) King(John) Vy Greedy(y) Brother(Richard,John) it seems obvious that Evil(John),but propositionalization produces lots of facts such as Greedy(Richard)that are irrelevant With p k-ary predicates and n constants,there are p.n instantiations With function symbols,it gets nuch much worse! Chapter 99
Problems with propositionalization Propositionalization seems to generate lots of irrelevant sentences. E.g., from ∀ x King(x) ∧ Greedy(x) ⇒ Evil(x) King(John) ∀ y Greedy(y) Brother(Richard, John) it seems obvious that Evil(John), but propositionalization produces lots of facts such as Greedy(Richard) that are irrelevant With p k-ary predicates and n constants, there are p · nk instantiations With function symbols, it gets nuch much worse! Chapter 9 9
Unification We can get the inference immediately if we can find a substitution 0 such that King(x)and Greedy(x)match King(John)and Greedy(y) 0={/John,y/John}works UNIFY(a,B)=0 if a0=30 le Knows(John,x)Knows(John,Jane) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y)】 Knows(John,x) Knows(x,OJ) Chapter 9 10
Unification We can get the inference immediately if we can find a substitution θ such that King(x) and Greedy(x) match King(John) and Greedy(y) θ = {x/John, y/John} works Unify(α, β) = θ if αθ = βθ p q θ Knows(John, x) Knows(John, Jane) Knows(John, x) Knows(y, OJ) Knows(John, x) Knows(y, Mother(y)) Knows(John, x) Knows(x, OJ) Chapter 9 10