第四章 归结推理方法(ppt课件).ppt

第三章归结原理(第二部分) (Chapter 3 Resolution Reasoning)(Part B)
徐从富
浙江大学人工智能研究所
2002年第一稿
2004年9月修改
1
本章的主要参考文献:
[1] 石纯一等. 《人工智能原理》. 清华大学出版社, 1993. pp11-81. (【注意】:本课件以该书中的这部分内容为主而制作,若想更加全面地了解归结原理及其应用,请参见如下文献[2]和[3])
[2] 陆汝钤. 《人工智能》(下册). 科学出版社, 2000. pp681-728.
[3] 王永庆. 《人工智能原理与方法》. 西安交通大学出版社, 1998. pp111-155.
【注】:若对定理的机械化证明的更多内容感兴趣者,可参考陆汝钤. 《人工智能》(下册). 科学出版社, 2000. pp729-788. 其最新进展可参考我国数学家吴文俊院士的相关论文,不过,他的研究工作对数学要求很高!
2
前言
命题逻辑的归结法
子句型
Herbrand定理
归结原理
3
归结(resolution)(也称消解)推理方法:
这是一种机械化的可在计算机上加以实现的推理方法。AI程序设计语言Prolog就是基于归结原理的一种逻辑程序设计语言。
4
归结法(也称消解法)的本质是一种反证法。

为了证明一个命题A恒真,要证明其反命题~A恒假。所谓恒假就是不存在模型,即在所有的可能解释中,~A均取假值。但一命题的解释通常有无穷多种,不可能一一测试。为此,Herbrand建议使用一种方法:从众多的解释中,选择一种代表性的解释,并严格证明:任何命题,一旦证明为在这种解释中取假值,即在所有的解释中取假值,这就是Herbrand解释。
5
命题逻辑的归结法
要证明: A1∧A2∧A3B 是定理(重言式)
 A1∧A2∧A3 ∧~B 是矛盾(永假)式
归结推理方法就是从A1∧A2∧A3 ∧~B 出发,使用归结推理规则来寻找矛盾,最后证明定理成立。归结法(消解法)的本质是数学中的反证法,称为“反演推理方法”。
等价于
6
建立子句集
首先,把A1∧A2∧A3 ∧~B化成一种称作子句形的标准形式。
如:
P∧(Q∨R)∧(~P∨~Q)∧(P∨~Q∨R)
然后将合取范式写成集合的表示形式,得
S = {P, Q∨R, ~P∨~Q, P∨~Q∨R}, 以“,”代
替“∧”。
子句集
一个子句
7
归结式
设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的归结式
8

子句集S
归结推理规则
S′=空子句□
S′=所得归结式
说明S是不可满足的
与S对应的定理成立
推理结束
是
否
9
例:证明(PQ)∧~Q~P
先将(PQ)∧~Q∧~(~P)
化成合取范式,得
(~P∨Q)∧~Q∧P
建立子句集
S={~P∨Q, ~Q, P)
对S作归结
~P∨Q
~Q
P
~P 1), 2) 归结
□ 3), 4) 归结
证毕
注:一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂得多,原因是要对量词和变量做专门的处理。
10