Inference in first-order logic课件.pptVIP

Backward chaining example 精品文档 Inference in first-order logic Chapter 9 精品文档 Outline Reducing first-order inference to propositional inference Unification Generalized Modus Ponens Forward chaining Backward chaining Resolution 精品文档 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 (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: ?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. 精品文档 Reduction contd. Every FOL KB can be propositionalized so as to preserve entailment (A ground sentence is entailed by new KB iff entailed by original KB) 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))) 精品文档 Reduction contd. Theorem: Herbrand (1930). If a sentence α is entailed by an FOL KB, it is entailed by a finite subset of the propositionalized KB Idea: For n = 0 to ∞ do create a propositional KB by instantiating with depth-$n$ terms see