Inference in first-order logic Chapter 9
Inference in first-order logic Chapter 9
Outline Reducing first-order inference to propositional inference ·Unification Generalized Modus Ponens ·Forward chaining ·Backward chaining ·Resolution
Outline • Reducing first-order inference to propositional inference • Unification • Generalized Modus Ponens • Forward chaining • Backward chaining • Resolution
Universal instantiation (Ul) Every instantiation of a universally quantified sentence is entailed by it: ∀va Subst([v/g},a) for any variable v and ground term g ·E.g.,∀k King(x)Greedy(x)→Evil(x)yields: King(John)Greedy(John)Evil(John) King(Richard)Greedy(Richard)=Evil(Richard)
Universal instantiation (UI) • Every instantiation of a universally quantified sentence is entailed by it: • v α Subst({v/g}, α) for any variable v and ground term g • E.g., x King(x) Greedy(x) Evil(x) yields: • • King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Richard) King(Father(John)) Greedy(Father(John)) Evil(Father(John))
Existential instantiation (El) For any sentence a,variable v,and constant symbol k that does not appear elsewhere in the knowledge base: 3va Subst({v/k},a) E.g.,3x Crown(x)^OnHead(x,John)yields: Crown(C1)OnHead(C1,John) provided C,is a new constant symbol,called a
Existential instantiation (EI) • For any sentence α, variable v, and constant symbol k that does not appear elsewhere in the knowledge base: • v α Subst({v/k}, α) • E.g., x Crown(x) OnHead(x,John) yields: Crown(C1 ) OnHead(C1 ,John) provided C1 is a new constant symbol, called a Skolem constant
Reduction to propositional inference Suppose the KB contains just the following: Vx 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
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