人工智能课程教学课件ch一阶逻辑中的推理.ppt

第九章、一阶逻辑中的推理 命题与一阶推理 量词的实例化（?和?） 如何将一阶推理简化为命题推理（命题化） 合一与提升 构造直接用于一阶语句的推理规则 前向链接 反向链接 归结 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), 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 if α is entailed by this KB Problem: works if α is entailed, loops if α is not entailed Theorem: Turing (1936), Church (1936) Entailment for FOL is semidecid