人工智能自动推理(第3部分 归结原理及其应用).ppt

1、3.8.1 命题逻辑中的归结法Resolution method in propositional logic,设有命题逻辑描述的命题F1，F2 ,Fn和G,要求来证明在F1F2Fn成立的条件下有G成立,或说F1F2Fn G是定理(重言式)，这就是我们的问题。如何建立推理规则，来证明这个定理便是我们的任务。 很显然F1F2Fn G是重言式等价于F1F2FnB是矛盾(永假)式。归结推理方法就是从F1F2FnB出发，使用归结推理规则来寻找矛盾，最后证明定理 F1F2Fn G 的成立。这种方法可称作反演推理方法。,子句与子句集 Clause and clause set,为使用归结方法，首先要把F1

2、F2FnG化成一种称作子句形的标准形式。一般地，归结推理规则所应用的对象是命题或谓词公式的一种特殊的形式，称为子句(Clause),一个子句就是一组文字的析取，一个文字或是一个原子(这时也称为正文字)，或者是一个原子的否定(这时也称为负文字)，如 都是文字， 是子句。,我们知道：对任意公式，都有与之等值的合取范式，即对任意公式 都有形如 的公式与之等价，其中每个 都是文字的析取式，就是一个子句。可以使用各种等价式将任意一个公式G转化为一个合取范式。例如，可以把公式 转换为如下的合取范式:,一个子句的合取范式(CNF形式)常常表示为一个子句的集合，即： 称为对应公式的子句集，其中每个元素都是一个

3、子句。把公式表示为子句集只是为了说明上的方便。,归结式Resolvent,命题逻辑的归结规则可以陈述如下。 设有两个子句: (其中 、 是子句, 是文字),从中消去互补对(即 和 ),所得的新子句: ，便称作子句 ， 的归结式，原子 称为被归结的原子。这个过程称为归结。没有互补对的两个子句没有归结式。 因此归结推理规则指的是对两个子句做归结，即求归结式。上述归结规则是一种合理的推理规则，这可从下述定理中看出。,定理3.2 子句 和 的归结式是 和 的逻辑推论。 证明：设 有 其中 和 都是文字的析取式。,假定 和 根据某种解释 为真。若 按 解释 为假，则 必不是单元子句(即单个文字),否则

4、按 解释为假。因此，按 必为真，即归结式 按 为真。 若 按I解释为真，则 按I为假，此时 必不是单元子句，并且 必按 为真，所以 按I为真。由此得出， 是 和 的逻辑推论。定理得证,Proof:,例3.3 计算下述子句的归结式： （1） 子句 中的文字 和子句 中 的文字是互补的。由 和 中分别删除 和 ,并且构造两个子句的其余部分 和 的析取式，得出归结式为 。 这两个被归结的子句可以写成： ,根据假言三段论，可以推出 ,它等价于 。因此可以知道假言三段论是归结的一个特例。,（2） 和 的归结式为 。因为 可以写作 ,所以可以知道假言推理也是归结的一个特例。 （3） 和 存在两个归结式，一

5、个是 另一个是: 。 在这个例子中，只能是在 上或 上进行归结，不能两者同时进行归结，也就是说 不是归结式。,（4） 中的任何文字都不能与 中的文字构成互补对，所以 和 不存在归结式。 （5） 和 是互补的，将它们分别由 和 中删除，再构造 和 其余部分的析取式，得出的归结式是空子句(Null clause)，用表示。这说明由于 和 的互补性，它们不能同时成立。所以空子句的出现代表出现了矛盾。,归结推理过程 Resolution reasoning procedure,从子句集S出发，仅只对S的子句间使用归结推理规则，并将所得归结式仍放入S中，进而再对新子句集使用归结推理规则，重复这些步骤直到

6、得到空子句，便说明S是不可满足的，从而与S对应的定理F1F2Fn G是成立的。 因为归结推理规则是正确的推理规则，归结式是原两子句的逻辑推论，于是归结过程出现空子句，说明S中必有矛盾。,例3.4 证明 先将 化成合取范式，得 建立子句集 对S做归结 (1) (2) (3) (4) （1）（2）归结 (5) （3）（4）归结 证毕。,3.8.2 谓词逻辑中的归结法 Resolution method in predicate logic,和命题逻辑一样，在谓词逻辑中也具有归结推理规则和归结反演过程。只是由于谓词逻辑中存在量词、个体变元等问题，使得谓词逻辑中的归结问题比命题逻辑中的归结问题复杂很多

7、。下面就来介绍谓词逻辑中的归结法。,子句型Clause form,归结证明过程是一种反驳程序，即：不是证明一个公式是有效的(valid)，而是证明公式之非是不可满足的(unsatisfiable)。这完全是为了方便，并且不失一般性。我们知道，归结推理规则所应用的对象是命题或谓词合式公式的一种特殊的形式，称为子句。因此在进行归结之前需要把合式公式化为子句式。 在第3.1节中已经介绍了如何把一个公式化成前束标准型 ,由于M中不含量词总可以把它变换成合取范式。无论是前束标准型还是合取范式都是与原来的合式公式等值的。,Skolem标准化过程,Step1: 化成前束范式:,Step2: 使用下述方法可以

8、消去前缀中存在的所有量词 令 是 中出现的存在量词 .,Case1:若在 之前不出现全称量词，则作置换: c/xr ，c是一个与M中出现的所有常量都不相同的新常量c，用c代替M中出现的所有xr，并且由前缀中删去 。,Case2:若在 之前出现全称量词 ，则选择一个与M中出现的任一函数符号都不相同的新m元函数符号f，用 代替M中的所有xr ，并且由前缀中删去 。,按上述方法删去前缀中的所有存在量词之后得出的公式称为合式公式的Skolem标准型。替代存在量化变量的常量c(视为0元函数)和函数f称为Skolem函数。,例3.5 化公式 为Skolem标准型。 在公式中， 的前面没有全称量词，在 的前

9、面有全称量词 和 ,在 的前面有全称量词 ， 和 。所以，在 中，用常数a代替x,用二元函数f(y,z)代替u,用三元函数g(y,z,v)代替w,去掉前缀中的所有存在量词之后得出Skolem标准型： (y)(z)(v)P(a,y,z, f(y,z),v, g(y,z,v),Skolem标准型的一个重要性质如下。 定理3.3 令 为公式 的Skolem标准型，则 是不可满足的，当且仅当 是不可满足的。 证明 不妨假设 已经是前束范式，即 设 为前缀中的第一个存在量词。令 其中， 是对应 的Skolem函数。我们希望证明 是不可满足的，当且仅当 是不可满足的。,设 是不可满足的。若 是可满足的，则

10、存在某定义域D上的解释I使 按I为真。即对任意 按I为真，所以，对任意 ，都存在元素 使 按I为真，那么G按I为真。这与G是不可满足的假设相矛盾。所以 必是不可满足的。,另一方面，设 是不可满足的。若G是可满足的，则存在某定义域D上的解释I使 按I为真。即对任意 ,存在元素 使 按I为真。扩充解释I，使得包括对任意 把 映射成 的函数f，即 扩充后的解释用I1表示。显然，对任意 按I1为真。即 ，这与 是不可满足的假设相矛盾。所以 必是不可满足的。,假设 中有m个存在量词。令 ，设 是在 中用Skolem函数代替其中第一个存在量词所对应的所有变量，并且去掉第一个存在量词而得出的公式,(k=1,

11、m),显然 。与上面的证明相似，可以证明 是不可满足的，当且仅当 是不可满足的(k=1,m)。所以可以断定， 是不可满足的，当且仅当 是不可满足的。,例3.6 的SKOLEM标准形与 并不是等值的。 考虑论域为D=1,2,这时 = 取 : P(1)=F P(2)=T 有 =T 而 的Skolem标准形： 设定a为1,这时 =F，与 不等值。 直观地说, 是 的一个具体的例化，考虑到存在量词有“或”的含义，然不能保证 真必有 真。 为真,只要在论域D中能找到一个个体 使 为真。而 =P(a)是从论域中选定一个个体a，这样不能保证P(a)为真。,显然 下不能决定 的真值，因为尚需对Skolem函数

12、f(1),f(2)做设定。或说 不是公式 的解释。若设定f(1)=2，f(2)=2方构成 的一个解释,例3.7 考虑 与 的逻辑关系。 仍在论域D=1,2上讨论。便有 取 ： 有 =T,然而 =F。同例3.6一样， 只是 的一个示例，不能保证 真 必真。 然而反过来却有 =T =T 也即 一般情形下有 总之， 与 并不等值，但在不可满足的意义下是一致的。而且 是 的逻辑推论，反过来不成立。,注意: 一个公式可以有几种形式的Skolem标准型。为简单起见，在变换公式时Skolem标准型时应该用尽量简单的Skolem函数代替G中存在量化的变量。即，应该使用变元个数量最少的Skolem函数。这意味着

13、，在化为前束标准型时，应该使存在量词尽量向左移。,例3.8 将合式公式化为子句形。 解：（1）消去蕴涵符号： 这可以利用等价式： 得到： （2）减少否定符号的辖域，把“ ”移到紧靠谓词的位置上： 这可以利用下述等价式：,得到： （3）变量标准化：重新命名变元名，使不同量词约束的变元有不同的名字： （4）消去存在量词：,（5）化为前束形： （6）把母式化为合取范式： （7）消去全称量词和连接词 ：,（8）更改变量名，有时称为变量分离标准化。于是有： 必须指出，一个子句内的文字可以含有变量，但这些变量总是被理解为全称量词量化了的变量。,一些概念 基原子(Ground atom)：不含变量的原子；

14、基文字(Ground literal)：不含变量的文字； 基子句(Ground clause)：不含变量的子句； 基子句集(Ground clause set)：不含变量的子句集； 基项(Ground item)：不含变量的项。 基例(Ground Instance)：如果一个表达式 中的变量被不含变量的项所替代得到不含变量的基表达式 ,则称 是 的基例。,另外，若 ,假设 的子句集为 。用 表示公式 的子句集,令 ,与定理3.3的证明方法相似，可以证明 是不可满足的，当且仅当 是不可满足的。即 不可满足 不可满足,例3.9 用Skolem标准型表达下述定理： 若对群 中的所有x有 ,则 是交

15、换群，其中“ ”为二元运算符，e为 中的么元。 我们首先与群论中的某些基本公理一起对上述定理进行符号化。群G满足下述4个公理： ，则 （封闭性） ，则 （结合律） 对所有的 （么元的性质） 对任意的 ，存在元素 ，使得 （逆元的性质）,令 表示 表示 ，则上述公式可表示为： 用 表示“若对所有 有 ，则 是可交换的，即对所有 ”。 可表示为：,这样所要证明的定理就是： 那么首先求出 和 的子句形，再求它们的并，便得到子句集合 ： 那么子句集,对命题逻辑应用归结原理的重要步骤是在一个子句中找出与另一子句中的某个文字互补的文字。对于不含变量的子句是容易做到的。当子句中含有变量时，问题要复杂很多。如

16、研究子句 中没有文字与 中的任何文字互补。但是若 在 中用 置换x，在 中用a置换y，便得出 其中 和 分别是 和 的基例。从上述例子可以看到，用适当的项置换 和 的变量可以产生新子句。,3.3.2 置换和合一 Substitution and Unification,定义3.5 置换(substitution)是形为 的有限集合，其中 是互不相同的变量，是不同于 的项（可以为常量、变量、函数） 表示用 置换 ，不允许 与 相同，也不允许 循环地出现在另一个 中。 当 是基项时，置换称为基置换(ground substitution)。不含任何元素的置换称为空置换(Null substitut

17、ion)，用 表示。,例如: 就是一个置换。但是， 不是一个置换，因为置换的目的是为了使某些变元被另外的变元、常量或函数取代，使之不再出现在公式中，而该置换在x和y之间出现了循环置换的情况，既没有消去x，也没有消去y。 定义3.6 令 为置换，E为表达式。设 是用项 同时代换E中出现的所有变量 而得出的表达式。 称为E的特例或例(Instance)。,例3.10 令 则有,定义3.7 令 为两个置换。和 复合也是一个置换，称为复合置换(composite substitution)，用 表示，它由在集合： 中删除下面两类元素得出的： ，当 ，当,例3.11 令 在构造 时，首先建立集合 由于

18、，所以要删除 。上述集合中的第三、四元素中的变量x，y都出现在x,y中，所以还应删除 。最后得出 不难验证出置换有下述性质。,(1) 空置换 是左么元和右么元，即对任意置换 恒有 (2) 对任意表达式E，恒有E( )(E ) 。 (3) 若对任意表达式E恒有E E ，则 。 (4) 对任意置换 ， ， 恒有 即置换的合成满足结合律。 (5) 设A和B为表达式集合，则 注意，置换的合成不满足交换律。,定义3.8 若表达式集合 存在一个置换 ，使得 则称集合 是可合一的(unifiable)，置换 称为合一置换(Unifier)。 例3.12 集合 是可合一的，因为 是它的合一置换。 例3.13

19、集合 是可合一的，因为 是它的合一置换。另外， 也是一个合一置换。所以合一置换是不唯一的。但是 比 更一般，因为用任意常量置换y都可以得到无穷个基置换。,定义3.9 表达式集合 的合一置换 是最一般的合一置换(MGU, Most General Unifier)，当且仅当对该集合的每个合一置换 都存在置换 使得 。 例如，在例3.13中，mgu = = ，但 不是mgu，并存在置换 ，有 。 例3.14 表达式集合P(x), P(y)，显然y/x与x/y都是该集合的mgu。这也说明mgu一般情况下也不是唯一的。但是它们除了相差一个置换名以外是相同的。,3.3.3 合一算法Unification

20、 algorithm,本节将对有限非空可合一的表达式集合给出求取最一般合一置换的合一算法。当集合不可合一时，算法也能给出不可合一的结论，并且结束。 研究集合 。集合中的两个表达式是不同的，差别是在P(a)中出现a,而在P(x)中出现x。为了求出该集合的合一置换，应首先找出两个表达式的不一致之处，然后再试图消除。对P(a)和P(x),不一致之处可用集合a,x表示。由于x是变量，可以取 ,于是有 ,即 是 的合一置换。,定义3.10 表达式的非空集合W的差异集(difference set)是按下述方法得出的子表达式的集合。 (1) 在W的所有表达式中找出对应符号不全相同的第一个符号(自左算起)。

21、 (2) 在W的每个表达式中，提取出占有该符号位置的子表达式。这些子表达式的集合便是W的差异集D。,例3.15 例如 的不一致集合为:,假设D是W的差异集，显然有下面的结论。 (1) 若D中无变量符号，则W是不可合一的。 例： (2) 若D中只有一个元素，则W是不可合一的 例： (3) 若D中有变量符号x和项t，且x出现在t中，则W是不可合一的。 例：,第一步 置 。,第二步 若 中只有一个元素，终止，并且 为W的最一般合一。否则求出 的差异集 。,第三步 若 中存在元素 和 ,并且 是不出现在 中的变量，则转向第四步。否则终止，并且W是不可合一的。,合一算法Unification algor

22、ithm,第四步 置 ，,第五步 置k=k+1，转向第二步。,注意:在第三步，要求 不出现在 中，这称为occur检查，算法的正确性依赖于它。,例3.16 求出 的最一般合一。 (1) (2) 未合一，差异集合为 。 (3) 中存在变量 和常量 。 (4) 令 ,(2) 未合一，差异集合为 。 (3) 中存在元素 ， ，并且变量x不出现在f(a)中。 (4) 令 = (2) 未合一，差异集合为 。 (3) 中的变量 不出现在 中。 (4)令 =,中只含有一个元素，所以 是 的最一般合一，终止。 注意，上述合一算法对任意有限非空的表达式集合总是能终止的。否则将会产生出有限非空表达式集合的一个无穷

23、序列 该序列中的任一集合 都比相应的集合 的少含一个变量(即， 含有 但 不含 )。由于 中只含有限个不同的变量，所以上述情况不会发生。这里不加证明地给出下述定理。 定理3.4 若W为有限非空可合一表达式集合，则合一算法总能终止在第二步上，并且最后的 便是 的最一般合一(MGU)。,利用归结法进行定理证明 To prove theorem using resolution method,归结原理指出了证明子句集不可满足性的方法。对于定理证明，经常见到的形式是： 这里， 是前提条件，而B则是逻辑结论。为了证明B是 的逻辑结论，只需证明 是不可满足的。又根据定理3.3，要证明公式的不可满足性，只要

24、证明其相应子句集的不可满足性即可。所以应用归结原理进行定理证明的步骤如下：,设要被证明的定理可用谓词公式表示为如下的形式: (1)首先否定结论B，并将否定后的公式B与前提公式集组成如下形式的谓词公式： (2) 求谓词公式G的子句集S。 (3) 应用归结原理，证明子句集S的不可满足性，从而证明谓词公式G的不可满足性。这就说明对结论B的否定是错误的，推断出定理的成立。,例3.20 已知: 求证: B是A的逻辑结论。,证明 首先将A和B化为子句集,下面进行归结： (6) （1）与（3）归结， (7)Q(b) （4）与（6）归结， (8) （5）与（7）归结 所以，B是A的逻辑结论。,例3.21 证明

25、“由梯形的对角线形成的内错角是相等的”。,首先定义谓词，并描述该问题所包含的知识。 T(x,y,u,v)：表示“xyuv是左上顶点为x,右上顶点为y，右下顶点为u，左下顶点为v的梯形(Trapezoid)”； P(x,y,u,v)：表示“线段xy平行(Parallel)于线段uv”； E(x,y,z,u,v,w)：表示“角xyz等于(Equal)角uvw”。,（由梯形的定义）,由上述公理应该能够断定 为真，即 为有效的公式。根据归结反演过程，否定该结论并且证明 是不可满足的。,于是由几何知识，有下述公理：,现在用归结证明S是不可满足的： （1） （2） （3） （4） （5） （2）和（4）的

26、归结式 （6） （5）和（1）的归结式 （7） （3）和（6）的归结式 最后一个子句是由S导出的空子句，可以断定S是不可满足的。,例3.22 “有些患者喜欢任一医生。没有任一患者喜欢任一庸医。所以没有庸医的医生”。 定义谓词为： P(x)：“x是患者patient”; D(x)：“x是医生doctor”; Q(x)：“x是庸医quack”，L(x,y)：“x喜欢(like)y”。 则前提和结论可以符号化如下： 目的是证明G是A1 和 A2 的逻辑结论，即证明 是不可满足的。,3.4.5 利用归结法进行定理证明,因此 的子句集合S为：,归结证明S是不可满足的： （1） （2） （3） （4） （

27、5） （6） （2）（4）归结 （7） （1）（3）归结 （8） （5）（7）归结 （9） （6）（8）归结,3.3.6 利用归结法进行问题求解To solve problem using resolution method,下面是利用归结原理求取问题答案的步骤： (1) 把已知前提条件用谓词公式表示出来，并化成相应的子句集，设该子句集的名字为S1。 (2) 把待求解的问题也用谓词公式表示出来，然后将其否定，并与一谓词ANS构成析取式。谓词ANS是一个专为求解问题而设置的谓词，其变量必须与问题公式的变量完全一致。 (3) 把问题公式与谓词ANS构成的析取式化为子句集，并把该子句集与S1合并构成子句集S。 (4) 对子句集S应用谓词归结原理进行归结，在归结的过程中，通过合一置换，改变ANS中的变元。 (5) 如果