第三章 归结原理 （第二部分） (Chapter 3 Resolution Reasoning) (Part B) 徐从富 浙江大学人工智能研究所 2002年第一稿 2004年9月修改

本章的主要参考文献： [1] 石纯一 等. 《人工智能原理》. 清华大学出版社, 1993. pp11-81. （【注意】：本课件以该书中的这部分内容为主而制作，若想更加全面地了解归结原理及其应用，请参见如下文献[2]和[3]） [2] 陆汝钤. 《人工智能》（下册）. 科学出版社, 2000. pp681-728. [3] 王永庆. 《人工智能原理与方法》. 西安交通大学出版社, 1998. pp111-155. 【注】：若对定理的机械化证明的更多内容感兴趣者，可参考陆汝钤. 《人工智能》（下册）. 科学出版社, 2000. pp729-788. 其最新进展可参考我国数学家吴文俊院士的相关论文，不过，他的研究工作对数学要求很高！

前言 命题逻辑的归结法 子句型 Herbrand定理 归结原理

归结（resolution)(也称消解）推理方法： 这是一种机械化的可在计算机上加以实现的推理方法。AI程序设计语言Prolog就是基于归结原理的一种逻辑程序设计语言。

归结法（也称消解法）的本质是一种反 证法。 为了证明一个命题A恒真，要证明其反命题~A恒假。所谓恒假就是不存在模型，即在所有的可能解释中，~A均取假值。但一命题的解释通常有无穷多种，不可能一一测试。为此，Herbrand建议使用一种方法：从众多的解释中，选择一种代表性的解释，并严格证明：任何命题，一旦证明为在这种解释中取假值，即在所有的解释中取假值，这就是Herbrand解释。

3.4 命题逻辑的归结法 要证明： A1∧A2∧A3B 是定理（重言式）  A1∧A2∧A3 ∧ ~B 是矛盾(永假)式 等价于

3.4.1 建立子句集 首先，把A1∧A2∧A3 ∧ ~B化成一种称作子句形的标准形式。 如： 3.4.1 建立子句集 首先，把A1∧A2∧A3 ∧ ~B化成一种称作子句形的标准形式。 如： P∧(Q∨R)∧(~P∨~Q)∧(P∨~Q∨R) 然后将合取范式写成集合的表示形式，得 S = {P, Q∨R, ~P∨~Q, P∨~Q∨R}, 以“,”代 替“∧”。 子句集 一个子句

没有互补对的两子句没有归结式，归结推理即对两子句做归结 3.4.2 归结式 设C1=P∨C1′ C2=~P∨C2′ 消去互补对，新子句 R(C1,C2) = C1′∨ C2′ 没有互补对的两子句没有归结式，归结推理即对两子句做归结 证明 C1∧C2R(C1,C2) 任一使C1，C2为真的解释I下必有R(C1,C2)也是真。 空子句□ 当C1=P C2=~P 两个子句的归结式为空，记作□，称为空子句，体现了矛盾。 为两个子句 子句C1、C2的归结式

3.4.3归结推理过程 子句集S 归结推理规则 S′=所得归结式 否 S′＝空子句□ 是 说明S是不可满足的 与S对应的定理成立 推理结束

例：证明(PQ)∧~Q~P 注：一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂得多，原因是要对量词和变量做专门的处理。 化成合取范式，得 (~P∨Q)∧~Q∧P 建立子句集 S={~P∨Q, ~Q, P) 对S作归结 ~P∨Q ~Q P ~P 1), 2) 归结 □ 3), 4) 归结 证毕 注：一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂得多，原因是要对量词和变量做专门的处理。

3.5 子句形 设有由一阶谓词逻辑描述的公式A1，A2，A3和B，证明在A1∧A2∧A3成立的条件下有B成立。仍然采用反演法来证明。 是不可满足的。与命题逻辑不同，首先遇到了量词问题，为此要将(3.2.1)式化成SKOLEM标准形。

3.5.1 SKOLEM标准形（即与或句） 对给定的一阶谓词逻辑公式 G=A1∧A2∧A3∧~B 第一步，化成与其等值的前束范式 [方法：参见2.3节“与或句演绎系统”] 第二步，化成合取范式 第三步，将所有存在量词（  ）消去

3.5.2子句与子句集 概念 原子公式：不含有任何联结词的谓词公式 文字：原子或原子的否定 子句：一些文字的析取 如，P(x) ∨~Q(x,y), ~P(x,c) ∨R(x,y,f(x)) 都是子句 由于G的SKOLEM标准形的母式已为合取范式，从而母式的每一个合取项都是一个子句，可以说，母式是由一些子句的合取组成的。 子句集S：将G的已消去存在量词的SKOLEM标准形，再略去全称量词，最后以“,”代替合取符号“∧”，便得子句集S。

例： 解：①将G化成SKOLEM标准形 G的子句集 子句集S中的变量，都认为是由全称量词约束着，子句间是合取关系。

3.5.3 建立子句集举例 第一类：代数、几何证明（定理证明） 例1.证明梯形的对角线与上下底构成的内错角相等 a(x) d(v) b(y) 3.5.3 建立子句集举例 第一类：代数、几何证明（定理证明） 例1.证明梯形的对角线与上下底构成的内错角相等 a(x) d(v) b(y) c(u)

证明： ①设梯形的顶点依次为a,b,c,d.引入谓词： T(x,y,u,v)表示以xy为上底，uv为下底的梯形 P(x,y,u,v)表示xy//uv E(x,y,z,u,v,w)表示∠xyz = ∠uvw ②问题的逻辑描述和相应的子句集为 梯形上下底平行： 平形内错角相等 已知条件 要证明的结论：B: E(a,b,d,c,d,b) 结论的“非”：S~B:~E(a,b,d,c,d,b)} 从而 S = {SA1, SA2, SA3, S~B }

第二类 机器人动作问题 (b) y (a) x (c) z 例2.猴子香蕉问题 已知一串香蕉挂在天花板上，猴子直接去拿是够不到的，但猴子可以走动，也可以爬上梯子来达到吃香蕉的目的。 初始状态S0 分析：问题描述，不能忽视动作的先后次序，体现时间概念。常用方法是引入状态S来区分动作的先后，以不同的状态表现不同的时间，而状态间的转换由一些算子（函数）来实现。

解： 引入谓词 引入状态转移函数 P(x,y,z,s): 表示猴子位于x处，香蕉位于y处，梯子位于z处，状态为s R(s): 表示s状态下猴子吃到香蕉 ANS(s): 表示形式谓词，只是为求得回答的动作序列而虚设的。 引入状态转移函数 Walk(y, z, s): 表示原状态s下，在walk作用下，猴子从y走到z处所建立的新状态。 Carry(y,z,s): 表示原状态s下，在Carry作用下，猴子从y搬梯子到z处所建立的新状态。 Climb(s): 表示原状态s下，在Climb作用下，猴子爬上梯子所建立的新状态。

初始状态为S0，猴子位于a，香蕉位于b,梯子位于c，问题描述如下： 猴子走到梯子处（从x  z） 猴子搬着梯子到y处 猴子爬上梯子吃到香蕉 初始条件 结论 walk

第三类 程序设计自动化问题 例3：简单的程序集合问题 若一台计算机有寄存器a,b,c和累加器A，要求自动设计实现 + (b)  c 第三类 程序设计自动化问题 例3：简单的程序集合问题 若一台计算机有寄存器a,b,c和累加器A，要求自动设计实现 + (b)  c 的程序。

解: 先引入谓词 问题描述 P(u,x,y,z,s):表示累加器A,寄存器a,b,c分别放入u,x,y,z时的状态为s Load(x,s):表示状态s下,对任一寄存器x来说,实现(x)A后的新状态 Add(x,s):表示状态s下,对任一寄存器x来说,实现(x)+(A)A后的新状态 Store(x,s):表示状态s下,对任一寄存器x来说,实现 (A)x后的新状态 问题描述 ((a)A):寄存器a中的值放入寄存器A中 ((b)+(A)A)

初始状态D下，累加器A与寄存器a,b,c中的数值 ((A)C) 初始状态D下，累加器A与寄存器a,b,c中的数值 结论 子句集 S={SA1,SA2,SA3,SA4,S~B} 

3.6 Herbrand定理 虽然公式G与其子句集S并不等值，但它们在不可满足的意义下又是一致的。亦即，G是不可满足的当且仅当S是不可满足的。（证明从略，石纯一《AI原理》P17~20). 由于个体变量论域D的任意性，以及解释的个数的无限性，对一个谓词公式来说，不可满足性的证明是困难的。 如果对一个具体的谓词公式能找到一个较简单的特殊的论域，使得只要在该论域上该公式是不可满足的，便能保证在任何论域上也是不可满足的，Herbrand域（简称H域）具有这样的性质。

3.6.1 H域 设G是已给的公式，定义在论域D上，令H0是G中所出现的常量的集合，若G中没有常量出现，就任取常量aD，而规定H0={a} Hi = Hi-1 U {所有形如f(t1,…,tn)的元素} 其中， f(t1,…,tn)是出现于G中的任一函数符号，而t1, t2, …,tn是Hi-1的元素，I=1,2,… H∞为G的H域。（或说是相应子句集S的H域） “可数集合” H∞是直接依赖于G的最多共有可数个元素的集合

例1. S={P(a),~P(x) ∨P(f(x))}

例2. S={P(x), Q(f(x,a)) ∨R(b)} 【注】：在S中出现函数f(x,a),仍视为f(x1,x2)的形式

概念 基原子 原子 基文字 文字 基子句 子句 基子句集 子句集 基例： 对： ① 基子句： ② 基例： :没有变量出现的

3.6.2 H解释 思想：由子句集S建立H域、原子集A， 使任一论域D上S为真的问题，化成了仅有可数个元素的H域上S为真的问题。子句集S在D上不满足问题成了H上不满足问题，这是很有意义的结果。

定理3.3.2(1) 设I是S的论域D上的解释，存在对应于I的H解释I*，使得S|I=T，必有S|I*=T。 定理3.3.2(2) 子句集S是不可满足的，当且仅当在所有的S的H解释下为假。 （ 注：该定理将S在一般论域上的不可满足问题化成了可数集上H上的不可满足问题，以上只需讨论在S的H∞上即可。） 定理3.3.2(3) 子句集S是不可满足的当且仅当对每个解释I下，至少有S的某个子句的某个基例为假。

3.6.3 语义树 例1：设子句集S的原子集A={P,Q,R} P ~P Q ~Q R ~R 图 语义树（二叉树） N0 N11 N12 N21 N22 N23 N24 N31 N32 N33 N34 N35 N36 N37 N38 P ~P Q ~Q R ~R 图 语义树（二叉树） I(N)表示：从根结点到结点N分枝上所标记的所有文字的并集。 I(N34)={P,~Q,~R}

例2： 解：H={a,f(a),f(f(a)),…} A={P(a),Q(a),P(f(a)),Q(f(a)),…} 图 无限语义树 N0 N11 N12 N21 N22 N23 N24 N31 N32 N33 N34 N35 N36 N37 P(a) ~P(a) Q(a) ~Q(a) P(f(a)) N38

完全语义树： 失败结点： 封闭树： 对所有结点N,（ ）,I(N)包含了A={A1,A2,…}中的 或~Ai，i=1,2,…,n。 如果结点N的I(N)使S的某一子句有某一基例为假，而N的父辈结点不能判断这个事实，就说N是失败结点。 封闭树： 如果S的完全语义树的每个分枝上都有一个失败结点，即为封闭树。

例2中的完全语义树即为封闭树。 P(a) ~P(a) Q(a) ~Q(a) P(f(a)) 图 封闭语义树 N0 N11 N12 N21 如，I(N2,2)={P(a),~Q(a)},使得S中，~P(a) ∨Q(a)为假。 I(N3,6)={~P(a), Q(a) ,~P(f(a))},使得S中的P(f(a))为假。 …… I(N4,1)={P(a),~Q(a)},使得~Q(f(y))为假。

3.6.4 Herbrand定理 一阶谓词描述 化成不满足问题 G化成SKOLEM形 一般论域D简化成H∞域上的讨论 引入语义树 A1∧A2 ∧A3→B 化成不满足问题 G= A1∧A2 ∧A3 ∧ ~B G化成SKOLEM形 S={ , , ,……} 一般论域D简化成H∞域上的讨论 引入语义树

★Herbrand给出的两个定理 定理3.3.4(1) 定理3.3.4(2) 子句集S是不可满足的，当且仅当对应于S的完全语义树都是一棵有限的封闭语义树。 （注：证明从略） 定理3.3.4(2) S是不可满足的，当且仅当存在不可满足的S的有限基例集。

▲应当指出： Herbrand定理给出了一阶逻辑的半可判定算法，即仅当被证定理是成立的，使用该算法可得证，否则，得不出任何结果。

补充：石纯一编著：《人工智能原理》P39~40 重言式子句可删除规则 S={P∨~P,C1,C2}S={C1,C2}. 单文字删除规则 S={L，L∨C1，~L ∨C2，C3，C4}S′={~L ∨C2，C3，C4}，删除含L的子句  S ={C2，C3，C4}，删除文字~L 纯文字删除规则 当文字L出现于S中，而~L不出现于S中，便说L为S的纯文字。 S中删除LS′=Ø，S可满足 S中删除LS′≠Ø，S′,S同时不可满足 分离规则 S={L∨A1)∧… ∧(L∨Am)∧(~L∨B1)∧ …∧(~L∨Bn)∧R （不含L和~L的子句等） S′={A1,…,Am,R} S′={B1,…,Bn,R} S不可满足 S′、 S′同时不可满足 ′ ′ ′ ′

3.7 归结原理 虽然Herbrandp定理给出了推理算法，但需逐次生成基例集 ，再检验 的不可满足性，常常难以实现。 1965年，Robinson提出了归结原理，是对自动推理的重大突破。

3.7.1 置换与合一 置换：是形为{t1/v1,…,tn/vn}的一个有限集。 空置换：不含任何元素的置换。 其中，vi是变量，而ti是不同于vi的项（常量、变量、函数） 且vi≠vj，（i≠j),i,j=1,2,…,n 例如，{a/x,b/y,f(x)/z},{f(z)/x,y/z}都是置换。 空置换：不含任何元素的置换。 令置换={t1/v1,t2/v2,…,tn/vn} E是一阶谓词 ① 作用于E，就是将E中出现的变量vi均以ti代入（i=1,2,…,n)，以E表示结果，并称为E的一个例。 ② 作用于项t，是将t中出现的变量vi以ti代入(i=1,…,n)，结果以t·表示。

例：={a/x, f(b)/y, u/z} E=P(x, y, z) t = g(x, y) 那么 E = P(a, f(b), u) t=g(a, f(b))

常使用的置换的运算是置换乘法（合成） 若 ={t1/x1,…,tn/xn} ={u1/y1,…,um/ym} 置换乘积·是新的置换，作用于E相当于先后对E的作用。 定义如下： 先作置换：{t1 · /x1 ,…, tn · /xn , u1 /y1,…,um/ym } 若yi{x1,…, xn}时，先从中删除ui/yi； ti· = xi时，再从中删除ti ·/ xi； 所设的置换称作与的乘积，记作·

{f(y)·/x, z·/y, a/x, b/y, y/z} 即 {f(b)/x, y/y, a/x, b/y, y/z} 解：先做置换 {f(y)·/x, z·/y, a/x, b/y, y/z} 即 {f(b)/x, y/y, a/x, b/y, y/z} 先删除a/x,b/y,再删y/y，得 · = {f(b)/x,y/z} 当 E = P(x,y,z)时， E = P(f(y), z, z), (E) = P(f(b), y, y) E(·) = P(f(b), y, y) (E) = E(·)

概念：合一 设有公式集{E1,…,Ek}和置换，使 称E1,…,Ek是可合一的，且称为合一置换（union replacement）。 E1  = E2 =…Ek  称E1,…,Ek是可合一的，且称为合一置换（union replacement）。 若E1,…,Ek有合一置换，且对E1,…,Ek的任一合一置换都有置换存在，使得 = · 便说是E1,…,Ek的最一般置换，记作mgu（most general replacement)

例1 E1=P(a,y),E2=P(x,f(b)),E1,E2可合一， ={a/x, f(b)/y},且是E1，E2的mgu. 例2 E1=P(x), E2=P(f(y)) 置换={f(a)/x, a/y}并不是E1、 E2的mgu， 而= {f(y)/x}才是E1、 E2的mgu，也可以说，是E1、 E2的最简单合一置换。

例3 E1=P(x), E2=P(y)。显然{y/x}和{x/y}都是E1 、E2的mgu，说明mgu不唯一。

求mgu的算法（最一般合一置换mgu) 令w={E1,E2}。 令k=0,w0=w,0=(空置换）。 如果wk已合一，停止，k=mgu。 否则找不一致集。 若Dk中存在元素vk,tk,其中vk不出现于tk中做 5 ，否则不可合一。 令k+1= k·{tk/vk} wk+1=wk{tk/vk} = wk+1。 k+1k 转 3。

例 w={P(a,x,f(g(y))),P(z,f(a),f(u))} 其中，E1=P(a,x,f(g(y))),E2=P(z,f(a),f(u)) 求 E1,E2的mug 解：(1) w={P(a,x,f(g(y))),P(z,f(a),f(u))}. (2) 0=,w0=w. (3) w0未合一，自左至右找不一致集，有D0={a,z}. (4)取v0=z,t0=a. (5)令1= 0，{t0/v0}= · {a/z} = {a/z}. w1=w01={P(a,x,f(g(y))),P(a,f(a),f(u))}. (3) ′w1未合一，不一致集D1={x,f(a)}. (4) ′取v1=x,t1=f(a). (5) ′令2= 1·{f(a)/x}={a·/z,f(a)/x}={a.z,f(a)/x} w2=w12={P(a),f(a),f(g(y)),p(a,f(a),f(u))}.

(3) ′w2未合一，不一致集D2 = {g(y),u}. (4) ′取v2 = u,t2=g(y). (5) ′令3= 2·{g(y)/u} = {a/z,f(a)/x}·{g(y)/u} = { a/z,f(a)/x,g(y)/u} . w3 = w23={P(a),f(a),f(g(y)),P(a),f(a),f(g(y)))} (3) ′w3已合一，这时 3={a/z,f(a)/x,g(y)/u} ，即为E1，E2的mgu. 注：不可合一的情况 ①不存在vk变量，如w={P(a,b,c),P(d,b,c)} ②不存在tk变量，如w={P(a,b),P(x,y,z)} ③出现不一致集为{x,f(x)}形 ′ ′ ′ ′ ′

3.7.2 归结式 在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消去互补对，但需考虑变量的合一和置换。 3.7.2 归结式 在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消去互补对，但需考虑变量的合一和置换。 二元归结式：设C1, C2是两个无公共 变量的子句， L1, L2分别是C1, C2的文字，若L1与~ L2有mgu ，则 (C1  - {L1 })  (C2  - {L2 }) 称作子句C1, C2的一个二元归结式，而L1, L2为被归结的文字。 【注意】：同命题逻辑下的归结式不同的是，先需对C1, C2有关变量作mgu，再消去互补对。同样有： C1  C2  R(C1, C2)

R(C1, C2) = Q(g(y))  ~Q(b)  R(x) R(C1, C2) = P(b)  ~P(g(y))  R(x) 例1 C1 = ~A(x)  B(x) C2 = A(g(x)) 【解】：先将C1的变量x改写为y，可得mgu = {g(x)/y}，作归结得R(C1, C2) = B(g(x))。 例2 C1 = P(x)  Q(x) C2 = ~P(g(y))  ~Q(b)  R(x) 【解】：可知有两个合一置换，故有两个二元归结式。 （1）当取  = {g(y)/x}时，得 R(C1, C2) = Q(g(y))  ~Q(b)  R(x) （2）当取  = {b/x}时，得 R(C1, C2) = P(b)  ~P(g(y))  R(x)

例3 C1 = P(x)  ~Q(b) C2 = ~P(a)  Q(y)  R(z) 【解】：这时要注意，求归结式不能同时消去两个互补对。 如在  = {a/x, b/y}下，得R(z)。这不是C1, C2的二元归结式。 最简单的例子是： C1 = P  Q， C2 = ~P  ～Q 若消去上述两个互补对便得空子句。但是C1, C2并无矛盾。这说明消去两个互补对的结果并不是C1, C2的逻辑推论了。因此，消去两个互补对结果不是二元归结式。

在对子句作归结前，可先考虑子句内部的化简，这便提出了子句因子的概念。 设 C = P(x)  P(f(y))  ~Q(x) 令  = {f(y)/x}，将置换使用于C，可使P(x), P(f(y))合一。显然C比C简单得多。 子句因子：若一个子句C的几个文字有mgu ，那么C的C称作子句C的因子。 定义：若C1, C2是无公共变量的子句，作 （1） C1, C2的二元归结式 （2） C1的因子和C2的二元归结式 （3） C1,和C2的因子的二元归结式 （4） C1的因子和C2的因子的二元归结式 这四种二元归结式都叫子句C1, C2的归结式，记作R(C1, C2)

R(C1, C2) = Q(g(g(a)))  Q(b) 例4 C1 = P(x)  P(f(y))  Q(g(y)) C2 = ~P(f(g(a)))  Q(b) 【解】：先作C1的因子，取  = {f(y)/x}，得C1的因子 C1 = P(f(y))  Q(g(y)) 于是C1, C2归结式为 R(C1, C2) = Q(g(g(a)))  Q(b) 【说明】：上述推理过程的正确性能得到保证。

3.7.3 归结推理过程 为证明AB成立，其中A, B是谓词公式，使用反演过程，先建立 G = A  ~B 3.7.3 归结推理过程 为证明AB成立，其中A, B是谓词公式，使用反演过程，先建立 G = A  ~B 进而做出相应的子句集S，只需证明S是不可满足的。 归结法是仅有一条推理规则的推理方法。对S中的可归结的子句作归结，求得归结式，并将这归结式（新子句）仍放入S中，反复进行这个归结过程直至产生空子句为止。这时S必是不可满足的，从而证明AB是成立的。 【注意】：归结推理的实例请详见石纯一等编著的《人工智能原理》pp48-51。

Thanks！ 2002年第一稿 2004年9月修改