人工智能四.ppt

Chapter 4. Resolution §4.1 Clausal Form §4.2 Unification §4.3 Resolution Principle §4.4 Resolution Procedure §4.5 Unsatisfactory Chapter 4. Resolution (continued) §4.6 True-or-False Questions §4.7 Fill-in-the-Blank Questions §4.8 Circuit Example §4.9 Mathematics Example §4.10 Soundness and Completeness §4.11 Resolution and Equality 归结 对于定理证明问题，可以用一阶谓词逻辑表示，即给定前提P和结论Q，证明P→Q。 需要对每一个解释进行验证。 可以使用上一章的推理过程进行推理。 但是中间结果数量庞大，而且可能无法推理出。 采用反证法。 P∧?Q→{}。 §4.1 Clausal Form 子句型是一种简化了的谓词演算，除了普通谓词演算符号外，还包括文字和子句。 文字：原子谓词公式及其否定统称为文字． 子句：任何文字的析取式称为子句． 空子句：不包含任何文字的子句称为空子句．记为：□或NIL Horn子句：至多包含一个正文字的子句。 子句集：由子句和空子句所构成的集合称为子句集． 子句型的生成过程 （1）删除蕴涵符 （2）否定内移 （3）变量标准化 （4）删除存在量词 （5）删除全称量词 （6）析取内移 （7）删除合取运算符 （8）变量更名 演示示例 演示示例（续） 同一变量只受 一个量词约束 演示示例（续） （4）删除存在量词 演示示例（续） （5）析取内移（化为合取范式） （6）删除全称量词 演示示例（续） （7）删除合取运算符 （8）变量更名 §4.2 Unification 合一：判定两个表达式通过适当的置换是否可以变成同一表达式的过程。 置换： 形如 建立了一个变量与表达式之间的关联 每一个变量至多与一个表达式相关联 被关联的变量不出现在任何关联的表达式中 如：{A/x, F(B)/y, w/z} 是置换；{G(y)/x, F(x)/y}不是置换。 Term 项是论域中的对象名，定义如下： 单独一个个体（常量或变量）是项； 若t1, t2, … , tn是项，f 是n 元函数，则f (t1, t2, … , tn )是项； 由1,２生成的表达式是项。 因此，项有三种类型：变量、常量或者函数表达式。 置换实例（例示） 置换的合成 设 合成运算举例 合一 合一 合一不一定唯一 E={P(a,y), P(x, f(b))} ?1={a/x, f(b)/y} (唯一) E={P(x,y), P(x,f(b))} ?1={a/x, f(b)/y} (不唯一) ?2={b/x, f(b)/y} 合一运算举例 差异集合 设W是非空表达式集合，W的差异集合D定义如下：首先找出W的所有表达式中不是都相同的第一个符号，然后从W的每个表达式中抽出占有这个符号位置的子表达式，所有这些子表达式组成的集合就是W的差异集合D。 例子: W={P(x,f(y,z),z，w), P(x,a), P(x, g(z),z,b)} D={f(y,z), a, g(z)} 合一算法（1） (1)令k=0, W0=W(W={E1, E2}), ? 0=? (2)如果Wk已经合一,则算法停止, ? k=mgu 否则，求出Wk的差异集Dk (3)如果Dk中存在元素xk , tk,xk是变元,tk是项,且xk不在tk中出现,则转(4)；否则不可合一，停止 (4)令 ? k+1= ? k ?{tk /xk} W k+1= W k{tk /xk}=W ? k+1 k=k+1 然后转(2) (5)算法终止，mgu不存在。 合一算法（2） 换名: {P(f(x), x), P(x, a)}; 如果不换名：D={f(x), x}. 换名: {P(f(y), y), P(x, a)}; mgu: {f(a)/x, a/y} 合一算法（3） 求W={P(a,x,f(g(y))), P(z,f(z),f(u))}的mgu. D0={a,z}， ? 1=