第3章 确定性推理方法课件

人工智能原理及应用第3章确定性推理方法

二零一二年元月AI&itsApplications第3章确定性推理方法确定性推理方法

知识是人工智能研究的一个核心问题，它包括两个方面：知识表示和知识推理，即如何在人工智能中清晰地表示人类的常识，并运用这些常识去进行符合人类行为的推理。按照推理过程所用知识的确定性，推理可分为确定性推理和不确定性推理。自然演绎推理和归结推理是经典的确定性推理，它们以数理逻辑的有关理论、方法和技术为理论基础，是机械化的、可在计算机上加以实现的推理方法。第3章确定性推理方法第3章主要内容3.1 推理概述

3.2 确定性推理的逻辑基础

3.3 演绎推理方法

3.4 归结推理方法

3.5 归结过程中的控制策略

第3章确定性推理方法3.1推理概述

3.1.1推理的概念

3.1.2推理的方法

3.1.3推理的控制策略

3.1.4推理中的冲突

第3章确定性推理方法3.1推理概述

3.1.1推理的概念

所谓推理是指按照某种策略从已知事实出发去推出结论的过程。知识推理是指在计算机或智能机器中，在知识表达的基础上，利用形式化的知识模型，进行机器思维求解问题，实现状态转移的智能操作序列。推理所用的事实可分为两种情况，一种是与求解问题有关的初始证据；另一种是推理过程中所得到的中间结论，这些中间结论可以作为进一步推理的已知事实或证据。例：①商品是用来交换的，所以，有些用来交换的是商品。②老虎是要吃人的，东北虎是老虎；所以，东北虎是要吃人的。智能系统的推理包括两个方面的基本问题：一个方面是推理的方法，另一个方面是推理的控制策略。第3章确定性推理方法3.1推理概述

3.1.2推理的方法

推理有很多种方法，根据知识表示方式分类分为“图搜索”方法及“逻辑论证”方法；根据逻辑基础分类可分为演绎推理、归纳推理、默认（缺省）推理；根据知识的确定性分类分为确定性推理与非确定性推理；根据推理过程的单调性分类分为单调推理、非单调推理。1．演绎推理：演绎推理是一种由一般到个别的推理方法，其核心是三段论，由一个大前提、一个小前提和一个结论这三部分组成的。其逻辑式为：大前提是已知的一般性知识或推理过程得到的判断；小前提是关于某种具体情况或某个具体实例的判断；结论是由大前提推出的，并且适合于小前提的判断。第3章确定性推理方法3.1推理概述

3.1.2推理的方法

1．演绎推理：例：有如下三个判断：①计算机系的学生都会编程序；（一般性知识）②程强是计算机系的一位学生；（具体情况）③因此程强会编程序。（结论）这是一个三段论推理。其中：“①计算机系的学生都会编程序”是大前提，“②程强是计算机系的一位学生”是小前提，那么“③程强会编程序”是经演绎推出来的结论。其结论蕴含在大前提中，这就是典型的演绎推理三段论。第3章确定性推理方法3.1推理概述

3.1.2推理的方法2．归纳推理归纳推理的基本思想是：先从已知事实中猜测出一个结论，然后对这个结论的正确性加以验证。例如常用的数学归纳法。归纳推理的类型按照所选取的事例的广泛性可分为完全归纳推理、不完全归纳推理。归纳推理按照推理所使用的方法可分为枚举归纳推理、类比归纳推理、默认推理等。（1）枚举归纳推理：是由已观察到的事物都有某属性，而没有观察到相反的事例，从而推出某类事物都有某属性。（2）类比归纳推理：指在两个或两类事物有许多属性都相同或相似的基础上，推出它们在其它属性上也相同或相似的一种归纳推理。（3）默认推理：称为缺省推理，它是在知识不完全的情况下假设某些条件已经具备所进行的推理。第3章确定性推理方法3.1推理概述

3.1.2推理的方法3．演绎推理与归纳推理的区别：演绎推理是在已知领域内的一般性知识的前提下，通过演绎求解一个具体问题或者证明一个结论的正确性。它所得出的结论实际上早已蕴含在一般性知识的前提中，演绎推理只不过是将已有事实揭露出来，因此它不能增殖新知识。归纳推理所推出的结论是没有包含在前提内容中的。这种由个别事物或现象推出一般性知识的过程，是增殖新知识的过程。4．推理的其它分类：（1）确定性推理与不确定推理（2）单调推理与非单调推理（3）启发式推理与非启发式推理第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略推理的控制策略是指如何使用领域知识使推理过程尽快达到目标的策略，主要是指推理方向的选择、推理时所用的搜索策略及冲突解决策略等。推理的控制策略包括推理策略和搜索策略。推理策略主要解决推理方向、求解策略、冲突消解策略等问题。搜索策略主要解决推理线路、推理效果、推理效率等问题。按照对推理方向的控制，推理可分为正向推理、反向推理、混合推理及双向推理四种情况。一般都要求系统具有三个要素：一个存放知识的知识库

一个存放初始事实和中间结果的数据库

一个用于推理的推理机第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.1正向推理正向推理是由已知事实出发，正向使用推理规则向结论方向的推理，算法步骤描述如下：（1）把用户提供的初始证据放入综合数据库；（2）检查综合数据库中是否包含了问题的解，若已包含，则求解结束，并成功推出；否则执行下一步；第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.1正向推理（3）检查知识库中是否有可用知识，若有，形成当前可用知识集，执行下一步；否则转(5)。（4）按照某种冲突消解策略，从当前可用知识集中选出一条规则进行推理，并将推出的新事实加入综合数据库种，然后转(2)。第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.1正向推理（5）询问用户是否可以进一步补充新的事实，若可补充，则将补充的新事实加入综合数据库中，然后转(3)；否则表示无解，失败退出。第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略例：请用正向推理完成以下问题的求解：假设知识库中包含有以下2条规则：

r1：

IFBTHENC

r2：

IFATHENB已知初始证据A，求证目标C。解：本例的推理过程如下：推理开始前，综合数据库为空。推理开始后，先把A放入综合数据库，然后检查综合数据库中是否含有该问题的解，回答为“N”。接着检查知识库中是否有可用知识，显然r2可用，形成仅含r2的知识集。从该知识集中取出r2，推出新的实事B，将B加入综合数据库，检查综合数据库中是否含有目标C，回答为“N”。再检查知识库中是否有可用知识，此时由于B的加入使得r1为可用，形成仅含r1的知识集。从该知识集中取出r1，推出新的实事C，将C加入综合数据库，检查综合数据库中是否含有目标C，回答为“Y”。

它说明综合数据库中已经含有问题的解，推理成功结束，目标C得证。第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.2反向推理反向推理是以某个假设目标作为出发点的一种推理，又称为目标驱动推理或逆向推理。反向推理过程如图：第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.2反向推理算法描述如下：（1）将要求证的目标（称为假设）构成一个假设集；（2）从假设集中选出一个假设，检查该假设是否在综合数据库中，若在，则该假设成立，此时，若假设集为空，则成功退出，否则仍执行(2)；若该假设不在数据库中，则执行下一步；（3）检查该假设是否可由知识库的某个知识导出，若不能由某个知识导出，则询问用户该假设是否为可由用户证实的原始事实，若是，该假设成立，并将其放入综合数据库，再重新寻找新的假设，若不是，则转(5)；若能由某个知识导出，则执行下一步；（4）将知识库中可以导出该假设的所有知识构成一个可用知识集；（5）检查可用知识集是否为空，若是，失败退出；否则执行下一步；（6）按冲突消解策略从可用知识集中取出一个知识，继续；（7）将该知识的前提中的每个子条件都作为新的假设放入假设集，然后转(2)。第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略例：请用反向推理完成以下问题的求解：假设知识库中包含有以下2条规则：

r1：

IFBTHENC

r2：

IFATHENB已知初始证据A，求证目标C。解：其推理过程如下：推理开始前，综合数据库和假设集均为空。先将初始证据A和目标C分别放入综合数据库和假设集，然后从假设集中取出一个假设C，查找C是否为综合数据库中的已知事实，回答为“N”。再检查C是否能被知识库中的知识所导出，发现C可由r1导出，于是r1被放入可用知识集。接着从可用知识集中取出r1，将其前提条件B作为新的假设放入假设集。检查B是否为综合数据库中的实事，回答为“N”。再检查B是否能被知识库中的知识所导出，发现B可由r2导出，于是r2被放入可用知识集。从可用知识集中取出r2，将其前提条件A作为新的假设放入假设集。然后从假设集中取出A，检查A是否为综合数据库中的实事，回答为“Y”。说明该假设成立，由于无新的假设，故推理过程成功结束，于是目标C得证。第3章确定性推理方法3.1推理概述

3.1.3推理的控制策略3.1.3.3正反向混合推理正向推理和反向推理相结合的推理方法称为正反向混合推理。混合推理的方法包括：1.先正向后逆向2.先逆向后正向3.双向混合第3章确定性推理方法3.1推理概述

3.1.4推理中的冲突在推理过程中，系统要不断地用数据库中的事实与知识库中的规则进行匹配，当有一个以上规则的条件部分和当前数据库相匹配时，就需要有一种策略来决定首先使用哪一条规则，这就是冲突解决策略。冲突解决策略实际上就是确定规则的启用顺序。常用排序方法有如下几种:（1）按专一性排序

（2）按规则排序（3）按数据排序

（4）按就近原则排序（5）上下文限制

（6）按匹配度排序（7）按条件个数排序第3章确定性推理方法3.2确定性推理的逻辑基础3.2.1命题公式的解释3.2.2等价式3.2.3永真蕴含式3.2.4前束范式与Skolem范式3.2.5置换与合一本节中要考虑在人工智能中如何利用谓词逻辑表示来完成由问题到结论的推理。第3章确定性推理方法3.2确定性推理的逻辑基础3.2.1命题公式的解释

定义3.1设D是谓词公式P的非空个体域，若对P中的个体常量、函数和谓词按如下规定赋值：（1）为每个个体常量指派D中的一个元素；（2）为每个n元函数指派一个从

到D的一个映射，其中（3）为每个n元谓词指派一个从

到{F，T}的映射。则称这些指派为P在D上的一个解释I。定义3.2对于谓词公式P，如果至少存在D上的一个解释，使公式P在此解释下的真值为T，则称公式P在D上是可满足的。第3章确定性推理方法3.2确定性推理的逻辑基础3.2.2等价式

定义3.3设P与Q是D上的两个谓词公式，若对D上的任意解释，P与Q都有相同的真值，则称P与Q在D上是等价的。如果D是任意非空个体域，则称P与Q是等价的，记作

。常用谓词公式的等价式包括：（1）双重否定律：

（2）交换律：

（3）结合律：

（4）分配律：

（5）摩根定律：

第3章确定性推理方法3.2确定性推理的逻辑基础3.2.2等价式常用谓词公式的等价式包括：（6）吸收律：

（7）补余律:（8）连词化归律:

（9）量词转换律:

（10）量词分配律:第3章确定性推理方法3.2确定性推理的逻辑基础3.2.3永真蕴含式

定义3.4对谓词公式P和Q，如果

永真，则称P永真蕴含Q，且称Q为P的逻辑结论，P为Q的前提，记作。常用永真蕴含式包括：（1）化简式：

（2）附加式：

（3）析取三段论：

（4）假言推理：

（5）拒取式：

第3章确定性推理方法3.2确定性推理的逻辑基础3.2.3永真蕴含式

常用永真蕴含式包括：（6）假言三段论：

（7）二难推理：

（8）全称固化：

其中，y是个体域中的任一个体，依此可消去谓词公式中的全称量词。（9）存在固化：

其中，y是个体域中某一个可以使

P(y)为真的个体，依此可消去谓词公式中的存在量词。第3章确定性推理方法3.2确定性推理的逻辑基础3.2.4前束范式与Skolem范式

范式分为两种：前束范式与Skolem范式。定义3.5设F为一谓词公式，如果其中的所有量词均非否定地出现在公式的最前面，且它们的辖域为整个公式，则称F为前束范式。一般形式：其中，

为前缀，它是一个由全称量词或存在量词组成的量词串；为母式，它是一个不含任何量词的谓词公式。例:定义3.6如果前束范式中所有的存在量词都在全称量词之前，则称这种形式的谓词公式为Skolem范式。例：第3章确定性推理方法3.2确定性推理的逻辑基础3.2.5置换与合一

1．置换：定义3.7置换是形如：的有限集合。其中，

是项，

是互不相同的变元；

表示用t1

替换x1，并且要求t1

与x1

不能相同，x1

不能循环地出现在另一个t1

中。定义3.8设

是一个置换，F是一个谓词公式，把公式F中出现的所有

换成

得到一个新的公式G，记作G=Fθ，称G为F在置换θ下的例示。第3章确定性推理方法3.2确定性推理的逻辑基础3.2.5置换与合一

1．置换：定义3.9设是两个置换。则θ与λ的合成也是一个置换，记作

。它是从集合:中删去以下两种元素：

①当

时，删去

②当

时，删去

最后剩下的元素所构成的集合。第3章确定性推理方法3.2确定性推理的逻辑基础3.2.5置换与合一2．合一：定义3.10设有公式集

若存在一个置换θ，可使:

则称θ是F的一个合一。称F1,F2,…,Fn是可合一的。定义3.11设

是公式集F的一个合一，如果对F的任一个合一

都存在一个置换

，使得

，则称

是一个最一般合一。第3章确定性推理方法3.3演绎推理方法3.3.1什么是演绎推理3.3.2演绎推理的特点基于规则的演绎推理是一种直接的推理方法。它不再把有关的知识转化为子句集，而是把有关问题的知识和信息划分为规则与事实两种类型。规则由包含蕴含形式的表达式表示，事实由无蕴含式的表达式表示，并画出相应的与/或图，然后通过规则进行演绎推理。第3章确定性推理方法3.3演绎推理方法3.3.1什么是演绎推理所谓自然演绎推理，在已知一组为真的事实条件下，直接运用命题和谓词逻辑的一系列基本规则或定律来推出结论，该过程称为自然演绎推理。基于规则的演绎推理可分为正向演绎推理、反向演绎推理和正反向混合演绎推理。第3章确定性推理方法3.3演绎推理方法3.3.1什么是演绎推理3.3.1.1正向演绎推理1．事实表达式及其与/或图正向演绎推理步骤如下：利用等价式P→Q与～P∨Q消去蕴含符“→”。把否定符号“～”移到每个谓词符号的前面。变量标准化，即重新命名变量，使不同量词约束的变量有不同的名字。引入Skolem函数消去存在量词。将公式化为前束形。略去全称量词(这时默认事实表达式中尚存的变量是全称量词量化的变量)。重新命名变量；使同一变量不出现在不同的主要合取式中。第3章确定性推理方法3.3演绎推理方法3.3.1.1正向演绎推理2．F规则在与/或形正向演绎系统中，通常要求F规则应具有如下形式：L为单文字，W为与/或形公式。其变换步骤如下：（1）暂时消去蕴含符号“→”。（2）把否定符号“～”移到紧靠谓词的位置上，使其作用域仅限于单个谓词。（3）引入Skolem函数，消去存在量词。（4）化成前束式，消去全部全称量词。（5）恢复蕴含式表示。第3章确定性推理方法3.3演绎推理方法3.3.1.1正向演绎推理3．规则正向演绎与/或树正向演绎系统要求目标公式用子句形表示。如果目标公式不是子句形，则需要化成子句形。规则正向演绎推理过程是先用与/或树把已知事实表示出来，然后再用F规则的前件和与或树的叶节点进行匹配，并通过一个匹配弧把匹配成功的F规则加入到与/或树中，依此使用F规则，直到产生一个含有以目标节点为终止节点的解图为止。第3章确定性推理方法3.3演绎推理方法3.3.1.1正向演绎推理3．规则正向演绎(1)命题逻辑规则演绎过程：例：设已知事实为：

F规则为：

目标公式为：命题逻辑的规则演绎过程第3章确定性推理方法3.3演绎推理方法3.3.1.1正向演绎推理3．规则正向演绎(2)谓词逻辑规则演绎过程例：设已知事实的与/或形表示为：F规则为：目标公式为：命题逻辑的规则演绎过程第3章确定性推理方法3.3演绎推理方法3.3.1什么是演绎推理3.3.1.2逆向演绎推理从目标表达式出发，反方向使用规则（B规则）对目标表达式的与或图进行变换，最后得到含有事实节点的一致解图。1．目标表达式的与或形表示：在基于规则的逆向系统中，要用对偶形式对目标表达式进行Skolem化。即消去全称量词，对受全称量词约束的变量用Skolem函数或者常量代替，省略存在量词，所有变量默认为受存在量词约束，并进行变量换名，使得目标公式的主析取元之间具有不同的变量名。第3章确定性推理方法3.3演绎推理方法3.3.2逆向演绎推理1．目标表达式的与或形表示：例：目标公式：

Skolem化后：

变量标准化：这个目标的与或图表示如图，其子句集可以从结束在端节点的解图集中读得：第3章确定性推理方法3.3演绎推理方法3.3.2逆向演绎推理2．规则的应用逆向演绎推理以逆向方式使用规则（称为B规则），要求规则化简为以下形式：其中，L为单文字，W是与或形；规则的激活取决于L和与或图叶节点的匹配。逆向系统演绎过程的结束条件是生成的与或图含有事实表达式，而事实表达式限制为文字的合取形式。当事实表达式有一个文字同与或图中某一个端节点所标记的文字（子目标）匹配上时，就可以通过匹配弧把事实文字加到图上。这样当最后得到的与或图包含一个结束在事实节点上的一致解图时，系统便结束演绎，一个一致解图是解图中匹配弧置换集具有合一复合置换的那个解图。第3章确定性推理方法3.3演绎推理方法3.3.2逆向演绎推理2．规则的应用例：下面通过一个简例说明逆向系统的演绎过程。设有如下事实：FIDO是一只狗FIDO不叫FIDO摆尾巴MYRTLE瞄瞄叫规则如下：摆尾巴的狗是友好的友好且不叫的是不令对方害怕的第3章确定性推理方法3.3演绎推理方法3.3.2逆向演绎推理2．规则的应用例：狗是动物猫是动物喵喵叫的是猫问题是：是否存在一只猫和一只狗，使这只猫不怕这只狗？即目标公式：第3章确定性推理方法3.3演绎推理方法3.3.2逆向演绎推理2．规则的应用解：解该问题的过程如图：得到解答语句：（它表示有一只名叫MYRTLE的猫和一只名叫FIDO的狗，这只猫不怕那只狗。）第3章确定性推理方法3.3演绎推理方法3.3.2演绎推理的特点正向演绎推理逆向演绎推理问题求解的描述事实文字与或形事实文字合取式规则L=>W规则W=>L目标文字析取形目标文字与或形初始与或图相应于事实表达式∨事实表达式的与或树相应于目标公式∧事实表达式的与或树演绎推理F规则事实--->目标B规则目标--->事实结束条件包含所有目标节点的一致解图以事实节点作为所有终节点的一致解图第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简3.4.2Herbrand（海伯伦）定理3.4.3Robinson（鲁宾逊）归结原理3.4.4利用归结推理进行定理证明3.4.5应用归结原理进行问题求解在谓词演算中，利用前面列出的等价式和永真蕴含式，可以从已知的一些公式推导出新的公式，这个导出的公式叫做定理，在推导过程中使用的推理规则序列就成了该定理的一个证明，而这种推导，就是归结推理方法。第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简定义3.12任何文字的析取式称为子句。定义3.13包含任何文字的子句称为空子句，表示为NIL。定义3.14由子句或空子句所构成的集合称为子句集。在谓词逻辑中，任何一个谓词公式都可以化成一个子句集。将谓词公式化为子句集的步骤如下：(1)消去连接词“→”和“↔”：(2)减少否定符号的辖域：(3)对变元标准化：在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用另外一个没有出现过的任意变元代替，使不同量词约束的变元有不同的名字。(4)化为前束范式：把所有量词都移到公式的左边，并且在移动时不能改变其相对顺序。第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简在谓词逻辑中，任何一个谓词公式都可以化成一个子句集。将谓词公式化为子句集的步骤如下：（5）消去存在量词;（6）化为Skolem标准形;（7）消去全称量词：由于母式中的全部变元均受全称量词的约束，并且全称量词的次序已无关紧要，因此可以省掉全称量词。（8）消去合取词：在母式中消去所有合取词，把母式用子句集的形式表示出来。（9）更换变量名称：对子句集中的某些变量重新命名，使任意两个子句中不出现相同的变量名。第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简例：将下列谓词公式化成子句集。解：转换过程遵照上述9个步骤。(1)(2)(3)(4)(5)(6)(7)第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简例：将下列谓词公式化成子句集。解：转换过程遵照上述9个步骤。(8)子句集为：(9)子句变量标准化后，最终的子句集为：第3章确定性推理方法3.4归结推理方法3.4.1子句集及其化简当原谓词公式为非永假时，它与其标准子句集并不等价。当原谓词公式为永假（或不可满足）时，其标准子句集则一定是永假的，即Skolem化并不影响原谓词公式的永假性。这个结论很重要，是归结原理的主要依据，可用定理的形式来描述。定理3.1设有谓词公式F，其标准子句集为S，则F为不可满足的充要条件是S为不可满足的。第3章确定性推理方法3.4归结推理方法3.4.2Herbrand（海伯伦）定理1．H域及其原子集：定义3.15H域：设G是谓词公式，定义在论域D上，令H0是G中所出现的常量的集合。若G中没有常量出现，就任取常量a∈D，而规定H0={a}；

其中f(t1,…,tn)是出现于G中的任一函数符号，而t1…tn是Hi-1的元素，i=1,2,…。规定H∞为G的H域。(或说是相应的子句集S的H域)。第3章确定性推理方法3.4归结推理方法3.4.2Herbrand（海伯伦）定理2．对H域的解释问题：定义3.16如果子句集S的原子集为A，则对A中各元素的真假值的一个具体设定都是S的一个H解释。定理3.2设I是S的论域D上的解释，存在对应于I的H解释

，使得若有

必有

。定理3.3子句集S是不可满足的，当且仅当所有的S的H解释下为假。定理3.4子句集S是不可满足的，当且仅当对每一个解释I下，至少有S的某个子句的某个基例为假。

第3章确定性推理方法3.4归结推理方法3.4.2Herbrand（海伯伦）定理3．Herbrand（海伯伦）定理

定理3.5设有谓词公式F，其标准形的子句集为S，则F不可满足的充要条件是S不可满足。Herbrand（海伯伦）定理如下：定理3.6子句集S不可满足的充要条件是：该子句集S在H域中的所有解释都为假。定理3.7子句集S不可满足的充要条件是存在一个不可满足的基子句集S′。

对Herbrand（海伯伦）定理一般通俗性解释是：如果一个一阶谓词公式是永真的，则该公式的机器定理证明求解计算可在有限步内实现证明；如果该公式不是永真的，则无法在有限步内实现证明。第3章确定性推理方法3.4归结推理方法3.4.2Herbrand（海伯伦）定理3．Herbrand（海伯伦）定理

例：对子句集

画出相应的语义树。解：第3章确定性推理方法3.4归结推理方法3.4.2Herbrand（海伯伦）定理3．Herbrand（海伯伦）定理

Herbrand定理用于语义树解释有：定理3.8子句集S是不可满足的，当且仅当对应于S的完全语义树都是一棵有限的封闭语义树。定理3.9子句集S是不可满足的，当且仅当存在不可满足的有限基例集（即存在有限个失败结点）。

Herbrand定理给出了一阶逻辑的半可判定算法。其中的“半”字指的是有条件下的判定算法，即仅当被证定理是成立的，使用该算法方可得证。而当被证定理并不成立时，使用该算法得不出任何结果。第3章确定性推理方法3.4归结推理方法3.4.3Robinson（鲁宾逊）归结原理归结原理由J.A.Robinson于1965年提出，又称为消解原理。该原理是Robinson在Herbrand理论基础上提出的一种基于逻辑的、采用反证法的推理方法。由于其理论上的完备性，归结原理成为机器定理证明的主要方法。1．命题逻辑中的归结原理：定义3.17若P是原子谓词公式或原子命题，则称P与～P为互补文字。定义3.18设C1与C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，则从C1和C2中可以分别消去L1和L2，并将二子句中余下的部分做析取构成一个新的子句C12，称这一过程为归结，所得到的子句C12称为C1和C2的归结式，而称C1和C2为C12的亲本子句。第3章确定性推理方法3.4归结推理方法3.4.3Robinson（鲁宾逊）归结原理1．命题逻辑中的归结原理：定理3.10归结式C12是其亲本子句C1和C2的逻辑结论。定理3.11推论：设C1和C2是子句集S上的子句，C12是C1和C2的归结式。如果把C12加入子句集S后得到新子句集S1，则S1和S在不可满足的意义下是等价的。即：

S是不可满足的

<=>S1是不可满足的根据上述定理，有归结推理过程如下：(1)对子句集S中的各子句间使用归结推理规则。(2)将归结所得的归结式放入子句集S中，得新子句集S′。(3)检查子句集S′中是否有空子句(NIL),若有则停止推理；(4)置S=S′，转步骤（1）。第3章确定性推理方法3.4归结推理方法3.4.3Robinson（鲁宾逊）归结原理2．一阶谓词逻辑中的归结原理定义3.19设C1和C2是两个没有相同变元的子句，

L1和L2分别是C1和C2的文字，如果

L1与

～L2有最一般合一

，则把：

称作子句

C1和C2的一个二元归结式，而

L1和L2是被归结的文字。

第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明对于给定的一个谓词公式集F，要证明谓词公式集F能推导出目标公式G，可应用归结原理证明步骤如下：（1）否定结论G，得到～G；（2）将前提条件F和～G转化为子句集S（3）应用归结原理，对子句集S反复进行归结，若能归结出空子句，则证明子句集S的不可满足性，也即F→G为真。第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明例："快乐学生"问题，假设：任何通过计算机考试并获奖的人都是快乐的任何肯学习或幸运的人都可以通过所有的考试张不肯学习但他是幸运的任何幸运的人都能获奖。求证：张是快乐的。第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明证明：先将问题用谓词表示如下：

R1:“任何通过计算机考试并获奖的人都是快乐的”

R2:“任何肯学习或幸运的人都可以通过所有考试”

R3:“张不肯学习但他是幸运的”

R4:“任何幸运的人都能获奖”结论“张是快乐的”的否定第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明证明：首先将每一个表示逻辑条件的谓词子句转换为子句集可以接受的Skolem标准形。由R1可得：(1)由R2可得

(2)

(3)由R3可得

(4)

(5)第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明证明：首先将每一个表示逻辑条件的谓词子句转换为子句集可以接受的Skolem标准形。由R4可得

(6)由结论可得(7)此为结论的否定第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明证明：根据以上7条子句，归结如下：(8)(1)(6)归结(9)(8)(7)归结

(10)(9)(5)归结(11)(10)(3)归结(12)NIL(11)(5)归结原题得证。第3章确定性推理方法3.4归结推理方法3.4.4利用归结推理进行定理证明证明：其归结反演树如图：第3章确定性推理方法3.4归结推理方法3.4.5应用归结原理进行问题求解应用归结原理不仅可以进行结论的证明，同时也可以利用归结原理进行问题的求解。步骤如下：（1）把已知前提条件用谓词公式表示出来，并化成相应的子句集，设该子句集的名字为S1。（2）把待求解的问题也用谓词公式表示出来，然后将其否定，并与一谓词ANSWER构成析取式。谓词ANSWER是一个专为求解问题而设置的谓词，其变量必须与问题公式的变量完全一致。（3）把问题公式与谓词ANSWER构成的析取式化为子句集，并把该子句集与S1合并构成子句集S。（4）对子句集S应用谓词归结原理进行归结，在归结的过程中，通过合一置换，改变ANSWER中的变元。（5）如果得到归结式ANSWER，问题的答案即在ANSWER谓词中。第3章确定性推理方法3.4归结推理方法3.4.5应用归结原理进行问题求解例：求解问题,已知:如果x和y是同班同学,则x的老师也是y的老师；

王先生是小李的老师；

小李和小张是同班同学；

问小张的老师是谁?解：定义谓词

：x是y的老师；

：x与y是同班同学；则已知可表示成如下的谓词公式：第3章确定性推理方法3.4归结推理方法3.4.5应用归结原理进行问题求解例：以上谓词公式及结论的反化成子句集如下:①～C(x,y)∨～T(z,x)∨T(z,y)②

③

④

⑤

①②归结⑥

④⑤归结⑦NIL③⑥归结说明zhang的老师存在.第3章确定性推理方法3.4归结推理方法3.4.5应用归结原理进行问题求解例：为了求解用一个重言式代替④：④

用重言式代替结论的否定,恒为真⑤

①②归结⑥

④⑤归结⑦

③⑥归结可得到问题的结果:张的老师是王先生。也可用辅助谓词ANS(u)④