人工智能：3.4 归结演绎推理

 

归结演绎推理是一种基于鲁宾逊(Robinson) 归结原理的机器推理技术。鲁宾逊归结原理亦称为消解原理，是鲁宾逊于 1965 年在海伯伦(Herbrand) 理论的基础上提出的一种基于逻辑的 “反证法 ”。在人工智能中，几乎所有的问题都可以转化为一 个定理证明问题。而定理证明的实质，就是要对前提 P 和结论 Q ，证明 P ®

Q 永真。要证明 P
® Q 永真，就是要证明 P ® Q 在任何一个非空的个体域上都是永真的。这将是非常困难的，甚至是不可实现的。为此，人们进行了大量的探 索，后来发现可以采用反证法的思想，把关于永真性的证明转化为关于不可满足
性的证明。即要证明 P ® Q 永真，只要能够证明 P ∧¬Q 是不可满足的就可以了。

 

・52 ・

第 3 章   基本推理原理

在这一方面最有成效的工作就是海伯伦理论和鲁宾逊归结原理。海伯伦理论为自动定理证明奠定了理论基础，鲁宾逊归结原理使定理证明的机械化成为现实。他们的这些研
究成果，在人工智能的发展史上都占有很重要的历史地位。

 

3.4.1        
子句集及其化简

无论是海伯伦理论，还是鲁宾逊归结原理，都是在子句集的基础上讨论问题  的 ，因此在讨论归结演绎推理的理论和方法之前
，需要先介绍子句集的有关概念。

1.     子句和子句集

原子谓词公式或者其否定统称为文字。任何文字的析取式称为子句。不包含任何文字的子句称为空子句。空子句一般被记作 □或 NIL 。由子句或空子句所构成的集合称为子句集。

2.     谓词公式转换成相应的子句集的步骤

在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相 应的子句集，其转换步骤如下。

(1)     
消去连接词“®
”和“«
”。反复使用如下等价公式 ：

P ® Q Û
¬P ∨Q

P « Q Û
(P ∧Q)
∨(¬P ∧¬Q)

即可消去谓词公式中的连接词 “® ”和“« ”。例如， 公式[(A ® B )® B ] ∨C ，在消去蕴 涵符号后得到公式[ ¬ (¬A ∨B ) ∨B ]∨C 。

(2)     
减少否定符号的辖域。反复使用双重否定律

¬ (¬P ) Û P

摩根律                                        ¬
(P
∨Q) Û ¬P ∧¬Q

¬ (P ∧Q) Û ¬P ∨¬Q

量词转换律                      ¬
( “ x)P Û ( $ x) ¬P

¬ ( $
x)P Û ( “ x) ¬P

将每个否定符号“¬”移到仅靠谓词的位置
，使得每个否定符号最多只作用于一个谓

 

・53 ・

人工智能技术与方法

词。例如， 公式¬ ( “ x)( $ y )( “ z)[(A ∨B )∧¬ C] ，在 经过减少否定符号的辖域后得到的 公式为( $ x)( “ y)( $ z)[( ¬A ∧¬B ) ∨C]
。

(3)      对变元标准化。

在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用另外一个没有出现过的任意变元代替，使不同谓词约束的变元有不同的名字。

(4)      消去存在量词。

消去存在量词时，需要区分以下两种情况 ： 若存在量词不出现在全称量词的辖域内( 即它的左边没有全称量词) ，只要用一个新的个体 常 量（称为 Skolem 常量） 替换受该存在量词约束的变元，就可消去该存在量词
； 若存在量词位于一个或多个全称量词的辖域内，则需要用 Skolem 函数替换受该存在量词约束的变元，然后再消去该存在量词。例如， ( $ z)( “ y)(
$ x)P (x ,y ,z)
被( “ y)P (g(y),y ,A) 代替，其中g(y )为 Skolem 函数， A 为 Skolem 常量 。再例 如 ， 公式

(
$ z)( “ y){( $ x)P (x ,y,z)∨(
$ q)( “ w)( $ e)Q(q,w,e,z)}

在消去存在量词后， 变
为

(
“ y){P (g₁(y
),y ,A)∨( “ w)Q(g₂(y ),w,g₃(y
,w),A )}

其中， g₁(y ) 、g₂(y )和 g₃(y ,w) 为 Skolem 函数； A 为 Skolem 常量 。

(5)      化为前束范式。

化为前束范式的方法是把所有量词都移到公式的左边，并且在移动时不能改 变其相对顺序。由于第(3) 步已对变元进行了标准化，每个量词都有自己的变元， 这就消除了任何由变元引起冲突的可能，因此这种移动是可行的。

(6)      化为 Skolem 标准形。

Skolem 标准形的一般形式为

( “ x₁)( “ x₂) ⋯( “ x_n)M (x
₁，x ₂ ，⋯， x _n)

其中， M (x ₁，x ₂ ，⋯， x
_n)
是 Skolem 标准形的母式，它由子句的合取所构成。把谓词公式化为
Skolem 标准形可能需要使用以下等价关系
：

P
∨(Q∧R
) Û (P ∨Q) ∧(P
∧R )

(7)      消去全称量词。

由于母式中的全部变元均受全称量词的约束，并且全称量词的次序已无关紧 要，因此可以省掉全称量词。但剩下的母式，仍假设其变元是被全称量词量化的。

(8)      消去合取词。

・54 ・

第 3 章   基本推理原理

在母式中消去所有合取词，把母式用子句集的形式表示出来。其中，子句集中的每一个元素都是一个子句。例如 ， 用{(A ∨B ),(A ∨C)}
代替(A ∨B )∧(A ∨C)
。

(9)      更换变元名称。

对子句集中的某些变元重新命名，使任意两个子句中不出现相同的变元名。由于每一个子句都对应着母式中的一个合取元，并且所有变元都是由全称量词量化的，因此任意两个不同子句的变元之间实际上不存在任何关系。这样，更换变元名不会影响公式的真值。
例如，子句集

{¬P (x )∨¬P (y)∨P [f(x,y )],
¬P (x )∨Q[x ,g(x)],
¬P (x )∨¬P [g(x )]}

经更改变量名后，变为

{¬P (x ₁)∨¬P (y )∨P [f(x ₁,y )], ¬P (x₂)∨Q[x ₂,g(x₂)],
¬P (x ₃)∨¬P [g(x ₃)]}

3.     谓词公式转换成相应的子句集的例子

通过上述化简步骤，可以将谓词公式化简成一个标准子句集。下面给出谓词公式化简的一个完整的例子。设有谓词公式 ：

( “ x){P (x )→{(
“ y )[P (y )→P
(f(x
,y ))]∧Ø ( “ y)[Q(x,y
)→P (y
)]}}

消去连接词 →：

( “ x){ Ø P(x )∨{(
“ y)[ Ø P(y)∨P
(f(x,y))]∧Ø ( “ y)[ Ø Q(x ,y )∨P
(y )]}}

减少否定符号的辖域 ：

( “ x){ Ø P(x )∨{(
“ y)[ Ø P(y )∨P
(f(x,y))]∧(
$ y)[Q(x ,y
)∧Ø P(y )]}}

对变元进行标准化 ：

( “ x){ Ø P(x )∨{(
“ y)[ Ø P (y )∨P
(f(x
,y ))]∧( $ z)[Q(x,z)∧Ø P(z)]}}

消去存在量词 ：

( “ x){ Ø P(x )∨{(
“ y)[ Ø P(y )∨P
(f(x,y))]∧[Q(x,g(x
) )∧Ø P(g(x ))]}}

化为前束范式 ：

( “ x) ( “ y){ Ø P(x)∨{[
Ø P(y )∨P
(f(x
,y ))]∧[Q(x ,g(x )
)∧Ø P(g(x ))]}}

化为 Skolem
标准形：

( “ x)( “ y){[ Ø P(x)∨Ø P (y )∨P
(f(x,y
))]∧

[ Ø P(x )∨Q(x ,g(x
))]∧[ Ø P(x )∨Ø P(g(x ))]}

消去全称量词 ：

{[ Ø P(x )∨Ø P(y )∨P
(f(x
,y ))]∧[ Ø P(x)∨Q(x,g(x ))]∧[
Ø P(x)∨Ø P (g(x))]}

 

・55 ・

人工智能技术与方法

消去合取词 ：

{[ Ø P(x )∨Ø P(y )∨P
(f(x
,y ))],[ Ø
P(x)∨Q(x ,g(x
))],[ Ø P(x )∨Ø P(g(x ))]}

更换变元名称 ：

{[ Ø P(x )∨Ø P(y )∨P
(f(x
,y ))],[ Ø
P(u)∨Q(u,g(u))],[
Ø P(v)∨Ø P (g(v))]}

得到标准子句集 ：

{ Ø P(x )∨Ø P(y)∨P
(f(x,y)),
Ø P(u)∨Q(u,g(u))},
Ø P(v)∨Ø P (g(v))}

由于在消去存在量词时所用的 Skolem  函数可能不同，因此，化简后的标准子句集不是唯一的。这样，当原谓词公式为非永假时，它与其标准子句集并不等价。但是
，当原谓词公式为永假（即不可满足）时，其标准子句集则一定是永假的，即  Skolem  化并不影响原谓词公式的永假性。这个结论很重要，是归结原理的主要依据，它可用定理的形式来描述。

定理 3.1   设有谓词公式 F ，其相应的标准子句集为 S ，则 F 为不可满足的

充要条件是 S 为不可满足的。

由此定理可知，要证明一个谓词公式是不可满足的，只要证明其相应的标准子句集是不可满足的就可以了。至于如何证明一个子句集的不可满足性问题，则由下面的海伯伦理论和鲁宾逊归结原理来解决。

 

3.4.2        
海伯伦理论

要判定一个子句集是不可满足的，就是 要判定该子句集中的某一个子句是不可满足的。而要判定一个子句是不可满足的，则需要判定该子句对任何非空个体域上的任意解释都是不可满足的。可见，判定子句集的不可满足性是一项非常困难的工作。如果能对一个具体的谓词公式找到一个特殊的论域，使得该谓词公式只要在这个特殊的论域上不可满足，就能保证它在任意论域上也都为不可满足，
这将是十分有益的。针对这一情况，海伯伦构造了一个特殊的域，并且证明只要能对这个特殊域上的一切解释进行判定，就可得知子句集是否为不可满足的，这个特殊的域称为海伯伦域。

 

 

 

・56 ・

 

3.4.3        
鲁宾逊归结原理

第 3 章   基本推理原理

 

虽然 海伯伦提出了证明子句集不可满足性的理论，但要直接用它去证明子句集的不可满足性还是不现实的
，原因是海伯伦理论的计算量会随着 H
域中元素的增加而按指数规律增长，为此，鲁宾逊于  1965  年在海伯伦理论的基础上提出了归结原理。根据鲁宾逊归结原理只需对子句集中的子句做逐次归结，就可证明子句集的不可满足性，这是对定理
3.1 自动证明的一个重大突破。

1.     基本思想

Ø  谓词公式可以化成子句集 S ；

Ø 
子句集
S 中的子句之间为合取关系 ；

Ø 
只要有一个子句为不可满足的，则
S 为不可满足的 ；

Ø 
另外，空子句是不可满足的
；

Ø 
若 S 中包含有空子句，则一定是不可满足的。

鲁宾逊归结原理就是基于上述认识提出来的。其基本思想是 ： 首先把欲证明问题的结论否定，并加入子句集，得到一个扩充的子句集 S′，然后设法检验子句 集 S′是否含有空子句，若含有空子句，则表明 S′是不可满足的 ；若不含有空子句， 则继续使用归结法，在子句集中选择合适的子句进行归结，直至导出空子句或不 能继续归结为止。
这与数学中反证法的思想十分相似。

鲁宾逊归结原理可分为命题逻辑归结原理和谓词逻辑归结原理两种。无论是命题逻辑的归结，还是谓词逻辑的归结，都要涉及互补文字的概念，若
P 是原子谓词
公式，则称 P 与
Ø
P 为互补文字。

2.     命题逻辑的归结

归结推理的核心是求两个子句的归结式，因此需要先讨论归结式的定义和性质，然后再讨论命题逻辑的归结过程。

(1)      归结式的定义及性质。

设 C₁ 和 C₂ 是子句集中的任意两个子句，如果 C ₁ 中的文字 L₁ 与 C₂ 中的文字

L₂ 互补，那么可从 C ₁ 和 C₂ 中分别消去 L₁ 和 L₂ ，并将 C ₁ 和 C₂ 中剩下的部分按析

取关系构成一个新的子句 C ₁₂ ，称这一过程为归结，称 C ₁₂ 为
C₁ 和 C₂ 的归结式， 称
C₁ 和 C₂ 为 C₁₂ 的亲本子句。

・57 ・

人工智能技术与方法

例如，设 C₁=P ∨Q
， C₂= Ø P ∨R
，则 C₁₂ =Q ∨R 。

定理 3. 2     归结式 C₁₂ 是其亲本子句 C ₁ 和 C₂ 的逻辑结论。

证明      设 C₁=L∨C1¢ ， C₂=( Ø L)∨C¢2 关于解释 I  为真，需证明 C12  = C1¢ ∨C¢2 关

于解释 I
也为真。关于解释 I ，L
和 Ø L 二者必有一个为假，不妨先设 L 为假。由

于已知  L ∨C1¢ 为真，则 C1¢ 必为真。由于 C1¢ 必为真，所以 C1¢ ∨C¢2 必为真，即  C₁₂ 
必为真。同理，再设 Ø
L 
为假，则 C¢2 必为真， C1¢ ∨C¢2 必为真。显然，归结式 C₁₂ 是其亲本子句 C ₁ 和 C₂ 的逻辑结论。

例如，子句 P 与 Ø P ∨Q （即 P →Q ）的归结式为 Q ，这其实就是假言推理。再例如，子句 Ø
P ∨R （即 P →R ）与 Ø R ∨Q （即 R →Q ）的归结式为 Ø P ∨Q （即 P → Q ），这其实就是链式三段论。

推论   子句集 S={ C₁ ，C₂ ，⋯ ，C _n} 与子句集 S′={C₁₂ ，C₁ ，C₂ ，⋯ ，C _n} 的不 可满足性是等价的，其中 C
₁₂
为 C₁ 和 C₂ 的归结式。

这个推论说明，为证明子句集  S 
的不可满足性，只要对其中可进行归结的子句进行归结，并把归结式加入到子句集 S 中，或者用归结式代替他的亲本子句， 然后对新的子句集证明其不可满足性就可以了。如果经归结能得到空子句，根据空子句的不可满足性，即可得到原子句集
S 是不可满足的结论。

(2)      命题逻辑的归结反演。

归结原理给出了证明子句集不可满足性的方法。假设
F 为已知的前提条件，

G 为欲证明的结论，且 F 和 G 都是公式集的形式。根据反证法，可
把已知 F 证明
G 为真的问题，转化为证明
F ∧Ø G 为不可满足的问题。在不可满足的意义上，
公式集 F ∧Ø G 与其子句集是等价的 ，故又可把
F ∧Ø G 公式集上的不可满足问题，
转化为子句集上的不可满足问题。这样，就可用归结原理来进行定理  3.2  的自动证明。应用归结原理证明定理的过程称为归结反演。

在命题逻辑中，已知 F ，证明 G 为真的归结反演过程如下
：

①把 F
转化成子句集表示，得到子句集 S _F ；

②把目 标公式 G
的否定 Ø
G 也转化成子句集表示，并将其并入到 S _F 中，得到 S=S_F∪S
_ØG ；

③ 反复应用归结原理对子句集 S 中的子句进行归结，若出现空子句，则停止归结，此时就证明了
G 为真。

 

・58 ・

第 3 章   基本推理原理

例 3.4    设已知的公式集为{P ， (P ∧Q) →R ， (S ∨T)→Q ， T} ，求证结论 R
。

解  使用归结反演进行证明，先假设结论 R 为假，即¬R 为真 ； 将¬R 加入公式集，并化为扩展子句集 ：

S={P ， Ø P ∨Ø Q∨R
， Ø S∨Q
， Ø T∨Q
，T ， Ø R}

¬R

¬P∨ ¬Q Ú R

检验该子句集是否包含有空子句 ，若包含空子句，则表明 S
不可满足，即原假设 R
为假是错误的，从而证明 R
为真 。其归结过程可用归结演绎树表示，如图 3.1
所示。在该树中，由于根部出现空子句，因此命题可得到证明。

3.     谓词逻辑的归结

从命题逻辑的归结过程中看出 ，在求归结式时比较容易确定含有互补对文字的两

个子句
，这只要检查一下 L 和 Ø L 就可以了，

图 3.1 例 3.4 的归结反演树

因而匹配过程比较简单。而在谓词逻辑中，由于要考虑变量的约束问题，这一匹配过程就复杂多了，因而在应用归结法时，往往需对公式作变量置换和合一等处理，才能得到互补的基本式，以便进行归结。

设 C₁ 和 C₂ 为不具有完全相同变元的两个子句，子句中的变量已标准化。采用文字集的形式来表示子句( 即文字之间理解为析取关 系) ，则有

C₁={C_{1 i}}(i=1
，2 ，⋯， n )

C₂={C_2j}(j=1 ，2 ，⋯， m )

再设{L_{1 k}} 和{L_{2 k}}分别为 C₁ 和 C₂ 的两个子集。若{L_{1 k}} 和{L_{2 k}} 的并集存 在一个 mgu s ， 则两个子句的归结式为

C={{C_1i}
－{L_1k}}s∪{{C_2j}
－{L_2k}}

由于可有多种方法选取{ L_{1 k}} 和{L_2k} ，因此归结式不是唯一的。例如 ，

C₁ = P (x ，f(A ))∨P
(x ，f(y ))∨Q(y )

C₂ = Ø P(z ，f(A ))∨Ø Q(z)

若取 L₁₁ =
P (x ，f(A )) ，L₂₁
= Ø P (z ，f(A )) ，则存在 s={z/x } 使 L₁₁ 和 Ø L₂₁ 合一， 所以归结式为 P (z ，f(y ))∨Q(y )∨Ø Q(z) 。

 

・59 ・

人工智能技术与方法

若取 L₁₁ = P (x ，f(y )) ，L₂₁ = Ø P(z ，f(A )) ，则存在 s={z/x ，A
/y }
使 L₁₁ 和 Ø L₂₁

合一，所以归结式为 Q(A
) ∨Ø Q(z) 。

若取 L₁₁ = Q(y ) ，L₂₁ = Ø
Q(z) ，则存在 s={y /z} 使 L₁₁ 和 Ø L₂₁ 合一，所以归结式为 P (x ，f(A ))∨P
(x ，f(y ))∨Ø P(y ，f(A )) 。

这个例子说明，选择不同文字对做归结时可得到不同的归结式，但由于都是用最一般的合一作置换，因此这些归结式仍是最一般的归结式。就是说，如果对某个文字不是用  mgu 
来合一，那么得到的归结式比最一般的归结式有较多的限制。实际上，我们总是希望用最一般的归结式，以增加归结过程的灵活性。下面举几个简单的例子 说明谓词逻辑的归结过程。

例 3.5    已知： ①会朗读的人是识字的 ；

②海豚都不识字；

③有些海豚是很机灵的。证明： 有些很机灵的东西不会朗读。

证明 首先把问题用谓词逻辑描述如下
。已知： ① ( “ x)(R(x) ® L(x ))

②(
“ x)(D(x
) ® Ø L(x ))

③(
$ x)(D(x )∧I(x))

求证： ( $ x)(I(x
)∧Ø R
(x ))

再把前提条件的谓词公式及将要证明的结论的否定化成子句形式，求得子句集
：

S={ Ø R(x )∨L(x ) ， Ø D(y ) Ú Ø L(y) ， D(A ) ，I(A ) ， Ø I(z) Ú
R (z)}

图 3.2 所示的归结树代表一个可行的证明过程。由于根部出现空子句，因此命题可得到证明。

例 3.6    如图 3.3 所示，试证明梯形的对角线与上、下底构成的内错角相等。

 

 

 

 

 

 

 

・60 ・

第 3 章   基本推理原理

 

 

 

           ^{d                                    c}

图 3.2   例 3.5 的归结反演树                 图 3.3 例 3.6 梯形示意图

解  这是个初等几何问题，可先给出逻辑描述，建立子句集。设梯 形的顶点依次为 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
。则问题的逻辑描述和相应的子句集为

A ₁:( “ x)(
“ y)( “ u)(
“ v)[
T(x,y ,u,v )
® P (x ,y ,u,v )]   ( 梯形上、下底平行)

1

SA = { Ø T(x ,y ,u,v
) Ú P (x ,y,u,v
) }

A
₂: ( “ x)( “ y)( “ u)( “ v)[
P (x ,y,u,v )
® E(x,y,v ,u,v ,y )] ( 平行内错角相等)

2

SA ={ Ø P (x ,y ,u,v)
Ú E(x,y ,v ,u,v,y)
}

A
₃:T(a,b,c,d)        ( 已 知)

3

SA ={T(a,b,c,d)}

B
:E (a,b,d,c ,d,b)       (要证的结论)

S Ø B ={ Ø E(a,b,d,c,d,b)}

S
=
S_A1 L

S_A2 L

S_A3 L

SØB

图 3.4 所示的归结反演树代表一个可行的证明过程。由于根部出现空子句，
因此命题得到证明。

 

 

 

 

・61 ・

人工智能技术与方法

 

图 3.4 例 3.6 的归结反演树

若已知 x
=A ，那么 W(A ) 是否为真？对于这种问 题，可以使用刚才讨论的归结反演法证明。而对于 x
= ？时， W(A ) 为真这样的问题，则应先证明一个与回答问题语句中提问项有对应匹配关系的一般语句，然后找一个具体的匹配值，该值就 给出问题的回答 。这种要求产生满足条件的 x 的例子，需要用构造性的证明方法， 即如果能给出对问题的构造性证明过程，那么就可能给出具体问题的回答。

例 3.7 If Fido goes wherever John goes and
if John is at school,where is Fido? (John 去哪里，Fido 也去哪里，若 John
在学校，那么 Fido 在哪里？)

解  这个问题给出两个已知的事实和一个询问，这个问题的答案应从事实出

发演绎得到。先将问题用谓词公式表示 ：

前提公式集     (
“ x)(AT (John , x ) ® AT (Fido , x ))

AT (John , School)

目标公式          ( $ x)AT (Fido , x )

首先要证明目标公式是前提公式集的逻辑推论，然后找出一个 x
的例子，这样就回答了 Fido
在何处 的询问。关键是把询问表达为一个由存在量词约束的目标公式，这样就很容易用归结法给出证明。图 3.5 给出了该例的反演树。

 

图 3.5 例 3.7 的归结反演树

提取回答的步骤如下。

・62 ・

第 3 章   基本推理原理

(1)      用一个重言式来取代目标公式的否定式这个子句，该重言式为

Ø AT (Fido, x )∨AT(Fido, x )

(2)     
按反演树的构造进行归结，给出重言式来取代目标公式的否定式子句后的证明树，这时根子句不为空，称这样的证明树为修改证明树，
如图 3.6 所示。

 

 

图 3.6 修改证明树

(3)      用根部的子句作为回答语句。

从这个例子可以看出，回答的提取过程是把一棵归结反演树转化为根部带有回答语句的一棵修改证明树的过程。

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

・63 ・