经典逻辑推理学习课件

第４章经典逻辑推理

１、基本概念

２、自然演绎推理

３、归结演绎推理

４、与／或形演绎推理1第４章经典逻辑推理

１、基本概念

２、自然演绎推理

３、基本概念何为推理？从已知的事实出发，不断运用已掌握的（知识库中的）知识推出或归纳出新的事实（包括目标结论）的过程称为推理。人工智能中推理是由程序实现的，称这个程序为推理机。2基本概念何为推理？2推理方式及其分类人工智能作为对人类智能的模拟，有多种推理方式。它们是：１、演绎推理、归纳推理、默认推理２、确定性推理、不确定性推理３、单调推理、非单调推理４、启发式推理、非启发式推理５、基于知识的推理、统计推理、直觉推理。分别解释如下：3推理方式及其分类人工智能作为对人类智能的模拟，有多种推理方式１、演绎推理、归纳推理、默认推理

所谓演绎推理是从全称判断推导出特称判断的过程，是从一般到个别的推理。经常用的是三段论式，它包括：大前提：已知的一般性知识或假设；小前提：具体情况或个别事实；结论：由大前提推出的适合小前提所示情况的新判断。4１、演绎推理、归纳推理、默认推理

所谓演绎推理是从全称判断推１、演绎推理、归纳推理、默认推理

例如有如下三个判断：（１）足球运动员的身体都是强壮的；（２）高波是一名足球运动员；（３）所以，高波的身体是强壮的。其中（１）是大前提，（２）是小前提（３）是经演绎推出的结论。只要大前提和小前提是正确的，那麽由它们推出的结论就是正确的。5１、演绎推理、归纳推理、默认推理

例如有如下三个判断：5１、演绎推理、归纳推理、默认推理

演绎推理是人工智能中的一种重要推理方式，目前研制成功的各类智能系统中，大多是用演绎推理实现的。6１、演绎推理、归纳推理、默认推理

演绎推理是人工智能中的一种１、演绎推理、归纳推理、默认推理

归纳推理是从足够多的事例中归纳出一般性结论的推理过程，是一种从个别到一般的推理。例如，某厂进行产品质量检查，如果对每一件产品都进行了检查，并且都是合格的，则推导出结论：该厂生产的产品是合格的。并称这种推理为完全归纳推理。7１、演绎推理、归纳推理、默认推理

归纳推理是从足够多的事例中１、演绎推理、归纳推理、默认推理

如果是随机地抽查部分产品，并且它们是合格的，则得出结论该厂的产品是合格的，这种推理称为不完全归纳推理。默认推理又称为缺省推理，它是在知识不完全的情况下假设某些条件已经具备所进行的推理。例如，在条件Ａ已成立的情况下，如果没有足够的证据能证明条件Ｂ不成立，则默认Ｂ成立，并在默认前提下进行推理，推导8１、演绎推理、归纳推理、默认推理

如果是随机地抽查部分产品，１、演绎推理、归纳推理、默认推理

出某个结论来。由于这种推理允许默认某些条件是成立的，这就摆脱了需要知道全部有关事实才能进行推理的要求，使得在知识不完全的情况下也能进行推理。在默认推理过程中，如果到某一时刻发现原先所做的默认不正确，则可以撤消默认推理和所推出的结论，并重新按新情况进行推理。

9１、演绎推理、归纳推理、默认推理

出某个结论来。由于这种推２、确定性推理、不确定性推理

所谓确定性推理是指推理时所用的知识都是精确的，推出的结论也是确定的，是真或者是假。经典逻辑推理就属于这一种。不确定性推理是指推理时所用的知识不都是精确的，推出的结论也不完全是肯定的，其真值位于真与假之间，命题的外延模糊不清。10２、确定性推理、不确定性推理

所谓确定性推理是指推理时所用的２、确定性推理、不确定性推理

这里，我们特别强调的是不确定性推理。因为，人类思维活动的特征经常是在知识不完全的情况下进行多方位的思考及推理的。因此，要使计算机模拟人类的思维活动，就必须使它具有不确定性推理的能力。11２、确定性推理、不确定性推理

这里，我们特别强调的是不确３、单调推理、非单调推理所谓单调推理是指在推理的过程中随着推理的向前推进及新知识的加入，推出的结论是单调递增的趋势，并且越来越接近目标，推理过程不会出现反复的情况，即不会因新知识的加入否定了前面推出的结论，从而使推理又退回到前面的某一步。经典逻辑演绎推理属于这一种。12３、单调推理、非单调推理所谓单调推理是指在推理的过程中随着推４、启发式推理、非启发式推理若按推理中是否使用与问题有关的启发性知识，推理可分为启发式推理和非启发式推理。所谓启发性知识是指与问题有关并且能加快推理进程、求得问题最优解的知识。13４、启发式推理、非启发式推理若按推理中是否使用与问题有关的启５、基于知识的推理、统计推理、直觉推理如果从方法论的角度来划分，推理可分为基于知识的推理、统计推理和直觉推理。顾名思义，所谓基于知识的推理就是根据已掌握的事实，通过运用知识进行推理。统计推理是根据对某事物的数据统计进行推理。例如，对农作物的产量进行统计，从而得出是否增产的结论，从而找14５、基于知识的推理、统计推理、直觉推理如果从方法论的角度来划５、基于知识的推理、统计推理、直觉推理出增产和减产的原因。就是运用了统计推理。直觉推理又称常识性推理，是根据常识进行的推理。例如，当你从某建筑物下走过时，猛然发现有一物体坠落，这时你立即就会意识到这有危险，并立即躲开，这就是使用了直觉推理。目前直觉推理在计算机上的实现还是一件很困难的工作。15５、基于知识的推理、统计推理、直觉推理出增产和减产的原因。就推理的控制策略推理的控制策略主要包括推理方向、搜索策略、冲突消解策略、求解策略及限制策略等。推理方向用于确定推理的驱动方式，分为正向推理、逆乡向推理、混合推理及双向推理四种。16推理的控制策略推理的控制策略主要包括推理方向、搜索策略、冲突正向推理正向推理也称数据驱动推理，前向链推理、模式制导推理及前件推理等。正向推理过程的算法描述如下：１、将用户提供的初始已知事实送入数据库DB;2、检查数据库DB中是否包含问题的解，若有则求解结束，成功退出；否则执行下一步；17正向推理正向推理也称数据驱动推理，前向链推理、模式制导推理及正向推理３根据数据库DB中的已知事实，扫描知识库KB，检查KB中是否有可适用的知识，若有则转４，否则转６；４把KB中所有的适用知识都选出来，构成可适用的知识集KS；５若KS不空，则按某种冲突消解策略从中选出一条知识进行推理，并将推出的新事实加入DB中，然后转２；若KS空，转６；18正向推理３根据数据库DB中的已知事实，扫描知识库KB，检查K正向推理询问用户是否可以进一步补充新的事实，若可补充，则将补充的事实加入DB中，转３，否则表示求不出解，失败退出．算法的流程示意图如Ｐ115的图４－１所示．为了实现正向推理，还有很多实际问题需要解决，后面将陆续介绍．19正向推理询问用户是否可以进一步补充新的事实，若可补充，则将补逆向推理逆向推理的思想是首先假设一个目标，然后寻找支持该假设的证据，若所需的证据都能找到，则说明假设是成立的；若实在找不到证据时，说明原假设不成立，此时需另做假设．推理过程的算法如下所示．20逆向推理逆向推理的思想是首先假设一个目标，然后寻找支持该假设逆向推理１提出要求证的目标（假设目标）；２检查该目标是否已在数据库中，若在，则该目标成立，成功退出或者对下一目标进行检验；否则，转下一步；３判断该目标是否是证据，即它是否是由用户证实的原始事实，若是，则询问用户；否则转下一步４在知识库中找出所有能导出该目标的知识，形成适用知识集KS，转下一步；21逆向推理１提出要求证的目标（假设目标）；21逆向推理５从KS中选出一条知识，并将该知识的运用条件作为新的假设目标，然后转２．算法的示意图如Ｐ116的图４－２所示．

22逆向推理５从KS中选出一条知识，并将该知识的运用条件作为新双向推理混合推理就是在推理过程中合理地使用正向推理和逆向推理．混合推理的算法示意图如P11９的图４－４所示．

23双向推理混合推理就是在推理过程中合理地使用正向推理和逆向推求解策略和限制策略

所谓推理的求解策略是指只求一个解还是求所有解和最优解等．为了防止无穷的推理过程,以及由于推理过程太长增加时间及空间的复杂性，可在控制策略中指定推理的限制条件，以对推理的深度、宽度、时间、空间等限制。24求解策略和限制策略所谓推理的求解策略是指只求一个解还是求所模式匹配模式匹配是推理中必须进行的一项重要工作，因为只有经过模式匹配才能从知识库中选出当前适用的知识，才能进行推理。模式匹配可以有确定性匹配和不确定性匹配良种。所谓确定性匹配是指两个模式完全一样，或者通过代换后变得完全一致。所谓不确定性匹配是指两个知识模式不完全一样，但从总体上看它们的相似程度又落在规定的限度内。无论是确定性匹配还是不确定性匹配都需要进行变量的代换。25模式匹配模式匹配是推理中必须进行的一项重要工作，因为只有经过模式匹配例如设有如下两个知识模式：Ｐ1:father(李四，李小四）andman(李小四)Ｐ2:father(x,y)andman(y)若用李四代换x,用李小四代换y，则Ｐ1与Ｐ２就变得完全一样．若用这两个知识模式进行匹配，则是确定性匹配，也称完全匹配或精确匹配．26模式匹配例如设有如下两个知识模式：26模式匹配下面我们给出代换的概念：代换是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中，

t1，t2，…,tn是项，x1.，x2,…,xn是互不相同的变元；ti/xi表示用项ti代换变量xi，不允许ti和xi相同，也不允许xi循环的出现在另一个tj中。27模式匹配下面我们给出代换的概念：27模式匹配什麽是项呢？常可以作项，变量也可以作项，函数表达式可以作项。28模式匹配什麽是项呢？28模式匹配例如{a/x,f(b)/y,w/z}就是一个代换，但是{g(y)/x,f(x)/y}则不是一个代换，因为代换的目的是使某些变元被另外的变元、常量、或函数表达式取代，使之不再在公式中出现，而{g(y)/x,f(x)/y}在x与y之间出现了循环代换的情况，它既没有消去x,也没有消去y。29模式匹配例如{a/x,f(b)/y,w/z}就是一个代换，但模式匹配如果把它改为{g(a)/x,f(x)/y}就可以了，它将把公式中的x代换成g(a),y代换成f(g(a)),从而消去了变量x和y。

30模式匹配如果把它改为{g(a)/x,f(x)/y}就可以了，模式匹配下面给出一个公式的代换例式的概念：设F是一个公式，是一个代换，记F为公式F在下的代换例式，它是将公式F中的变量用中的项作代换的结果。例如有公式Ｆ＝Ｐ（x,y,f(y))和代换={a/x,b/y}于是F=Ｐ（a,b,f(b))31模式匹配下面给出一个公式的代换例式的概念：31模式匹配下面给出复合代换的定义设有两个代换和，其中={t1/x1,t2/x2,…,tn/xn}={u1/y1,u2/y2,…,um/ym}则此两个代换的复合也是一个代换，它是从＝{t1

/x1,t2

/x2,…,tn

/xn，u1/y1,u2/y2,…,um/ym}中删去如下两种元素：ti

/xi当ti

=xi时ui/yi

当yi

{x1.，x2,…,xn}时，后剩下的元素构成的集合，记为º。32模式匹配下面给出复合代换的定义32模式匹配例如设有如下代换：={f(y)/x,z/y}={a/x,b/y,y/z}求º和º解：我们先来求33模式匹配例如设有如下代换：33模式匹配={f(y)/x,z/y,a/x,b/y,y/z}={f(b)/x,y/y,a/x,b/y,y/z}去掉不合法的元素：y/y（条件１）

a/x,b/y（条件２）于是º＝{f(b)/x,y/z}34模式匹配={f(y)/x,z/y,a/x模式匹配再来求º，同样先求＝{a/x,b/y,y/z,f(y)/x,z/y}={a/x,b/y,z/z,f(y)/x,z/y}去掉不合法的元素z/z,f(y)/x,z/y得º={a/x,b/y}显然代换的复合运算是不可交换的。并且对任何代换存在空代换，并且º＝º＝35模式匹配再来求º，同样先求35模式匹配下面我们给出合一的概念：设有公式集F={F1，F2，…,Fn},若存在一个代换使得F1=F2=…=Fn则称为公式集F的一个合一，且称F1，F2，…,Fn是可合一的。36模式匹配下面我们给出合一的概念：36模式匹配例如F=P（x,y),={a/x,g(a)/y}求公式F在下的例式为F=P（a,g(a))对于公式集F={P（x,y，f(y)),P(a,g(x),z)}则={a/x,g(a)/y，f(g(a))/z}是公式F的一个合一。37模式匹配例如F=P（x,y),={a/x,g(a)/y模式匹配一个公式的合一一般是不唯一的。但如果是公式集F的一个合一，若对任一个合一都存在一个代换使得：=º则称是一个最一般合一。38模式匹配一个公式的合一一般是不唯一的。但如果38模式匹配最一般合一是唯一的。若用最一般合一去代换那些可合一的谓词公式，可使它们变成完全一致的公式。由此可知，为了使两个知识模式匹配，可用其最一般合一对它们进行代换。39模式匹配39模式匹配为了求最一般合一要用到一个差异集（也有叫分歧集的）的概念。设有如下两个谓词公式F1：P(x,y,z)F2:P(x,f(a),h(b))分别从F1与F2的第一个符号开始，逐个向右比较，此时发现F1中的y与F2中的f(a)不同，它们构成了一个差异集：D1={y,f(a)},40模式匹配为了求最一般合一要用到一个差异集（也有叫分歧集的）的模式匹配当继续向右比较时，又发现F1中与F2中的h(b)不同，于是又得到一个差异集：D2={z,h(b)}。下面给出求最一般合一的算法：（1）令K=0，Fk=F,k=这里，F是欲求其最一般合一的公式集，是空代换，它表示不做代换。（2）若Fk只含一个表达式，则算法停，k就是所求最一般合一。41模式匹配当继续向右比较时，又发现F1中与F2中的h(b)不同模式匹配（3）找出Fk的差异集Dk。（4）若Dk中存在元素xk和tk,其中xk是变元，tk是项,且xk不在tk中出现，则置：k+1=kº{tk/

xk}Fk+1=Fk{tk/

xk}K=k+1转（2）（5）算法停，F的最一般合一不存在。42模式匹配（3）找出Fk的差异集Dk。42模式匹配例如，设F={P(a,x,f(g(y))),P(z,f(z),f(u))}求其最一般合一．(1)令0=,F0=F,因F0中含有两个表达式，所以0不是最一般合一。(2)差异集D0={a,z},(3)1=0{a/z},F1={P(a,x,f(g(y))),P(a,f(a),f(u))}43模式匹配例如，设43模式匹配(4)D1={x,f(a)}(5)2=1{f(a)/x}={a/z,f(a)/x},F2=F1{f(a)/x}={P(a,f(a),f(g(y))),P(a,f(a),f(u))}。(6)D2={g(y),u}。(7)3=2{g(y)/u}={a/z,f(a)/x,g(y)/u}。44模式匹配(4)D1={x,f(a)}44模式匹配(8)F3=F2{g(y)/u}={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)/u))}={P(a,f(a),f(g(y)))}因为F3只含一个表达式了，所以3就是最一般合一，即{a/z,f(a)/x,g(y)/u}是最一般合一。45模式匹配(8)F3=F2{g(y)/u}45冲突消解策略接下来我们学习冲突消解方面的概念：在推理的过程中，系统不断的用以知的事实与知识库中的知识进行匹配，此时可能发生如下三种情况：（1）已知事实不能与知识库中的任何知识匹配成功。（2）已知事实恰好与知识库中的一条知识匹配成功。46冲突消解策略接下来我们学习冲突消解方面的概念：46冲突消解策略（3）已知事实可与知识库中的多条知识匹配成功。以上三种情况中，第一种情况使得推理无法进行下去，第三种情况则出现冲突，需要按一定的策略解决冲突。47冲突消解策略（3）已知事实可与知识库中的多条知识匹配成功。4冲突消解策略目前解决冲突的策略有多种，其基本思想都是对知识进行排序，常用的有以下几种：1、按针对性排序设有如下两条产生式规则：r1:IFA1andA2and…AnTHENH1r2:IFB1andB2and…BmTHENH248冲突消解策略目前解决冲突的策略有多种，其基本思想都是对知识进冲突消解策略如果存在最一般合一，使得r1中每一个Ai都可变成相应的Bi

，即r2中除了包含r1的全部条件A1,A2,…,An外，还包含其它条件，则称r2

比r1有更大的针对性，r1

比r2

有更大的通用性。一般选用针对性较强的产生式规则。(即应选用r2)因为它要求的条件较多，其结论一般更接近目标，一旦得到满足，可缩短推理过程。49冲突消解策略如果存在最一般合一，使得r1中每一个Ai都可变成冲突消解策略2、按已知事实的新鲜性排序在产生式系统推理过程中，每应用一条产生式规则就会得到一个或多个结论，数据库就会增加新的事实。把数据库后生成的事实称为新鲜的事实，即后生成的事实比先生成的事实具有较大的新鲜性。设规则r1可与事实组A匹配成功，规则r2可与事实组B匹配成功，则A与B中哪一组新鲜与它匹配的产生式规则就先被应用。50冲突消解策略2、按已知事实的新鲜性排序50冲突消解策略3、按匹配排序在不确定性匹配中，为了确定两个知识模式是否可以匹配，需要计算这两个模式的相似程度，当其相似程度达到某个预定的值时，就认为它们是可匹配的。若两条规则均按匹配度匹配成功，则匹配度大的那条规则优先启用。51冲突消解策略3、按匹配排序51冲突消解策略4、根据领域问题的特点排序某些领域问题可事先知道它的某些特性，可根据这些特性把知识排成固定的顺序。先匹配成功的优先启用的原则。52冲突消解策略4、根据领域问题的特点排序52冲突消解策略5、按上下文限制排序把产生式规则按它们所描述的上下文分成若干组，在不同的条件下，只能从相应的组中选取有关的产生式规则。这样可以减少冲突的发生53冲突消解策略5、按上下文限制排序53冲突消解策略6、按冗余限制排序若哪一条产生式规则被应用后产生冗余知识，则就降低它被应用的优先级。7、按条件个数排序如果有多条产生式规则生成的结论相同，则要求条件少的产生式规则被优先应用。54冲突消解策略6、按冗余限制排序544.2自然演绎推理从一组已知的事实出发，直接运用经典逻辑推理规则推出结论的过程称为自然演绎推理。其中，基本的推理规则是P规则、T规则、假言推理、拒取式推理等。假言推理的一般形式是P，PQQ拒取式的一般形式是PQ，QP554.2自然演绎推理从一组已知的事实出发，直接运用经典逻辑推4.2自然演绎推理以下是自然演绎推理的例子：例1：A，B，AC，BCD，DQQ1、AP规则2、ACP规则3、CT规则1和24、BP规则5、BCT规则3和4564.2自然演绎推理以下是自然演绎推理的例子：564.2自然演绎推理

6、BCDP规则7、DT规则5和68、DQP规则9、QT规则7和8问题得证574.2自然演绎推理6、BCDP规4.2自然演绎推理例2设已知如下事实；（1）凡是容易的课程小王（Wang)都喜欢。（2）C班的课程都是容易的。（3）ds是C班的一门课程求证小王喜欢ds这门课程。584.2自然演绎推理例2设已知如下事实；584.2自然演绎推理证明：首先定义谓词如下：Easy（x):x是容易的Like（x,y):x喜欢yC（x):x是C班的一门课程于是问题可以表示成：594.2自然演绎推理证明：首先定义谓词如下：594.2自然演绎推理x(Easy(x)Like(Wang,x))x(C(x)Easy(x))C(ds)Like（Wang,ds).604.2自然演绎推理x(Easy(x)Like(Wan4.2自然演绎推理1、x(Easy（x)Like（Wang,x))P规则2、Easy（ds)Like（Wang,ds)US规则和13、x(C（x)Easy（x))P规则4、C（ds)Easy（ds)US规则和35、C（ds)Like（Wang,ds)T规则2和46、C（ds)P规则7、Like（Wang,ds)T规则5和6即小王喜欢ds这门课程．614.2自然演绎推理1、x(Easy（x)Like（W4.2自然演绎推理自然演绎推理的优点是表达定理证明过程自然，容易理解，拥有丰富的推理规则，推理过程灵活，便于在推理过程中嵌入领域启发知识。缺点是容易产生组合爆炸，推理过程中得到的中间结论一般呈指数形式递增，这对于一个大型推理问题是十分不利的，甚至是不可能实现的。624.2自然演绎推理自然演绎推理的优点是表达定理证明过程自然，4.3归结演绎推理定理证明是人工智能的一个重要研究领域，这不仅仅是因为许多数学问题要通过定理证明得以解决，很多非数学问题（如医疗诊断、机器人规划及难题求解等）也都归结为一个定理证明问题。定理证明的实质是对前提P和结论Q证明PQ的永真性。但是证明一个谓词公式的永真性不像证明一个命题公式的永真性那麽简单，（它牵涉到谓词变量、客体变量及函数符号）在某些情况下甚至是行不通的。634.3归结演绎推理定理证明是人工智能的一个重要研究领域，这不4.3归结演绎推理在这种情况下，人们提出了用反证法来解决问题的思路。在这方面，海伯伦和鲁宾逊都作出了杰出的贡献。两人的研究都是以子句集为背景展开的。接下来，我们介绍这些概念。644.3归结演绎推理在这种情况下，人们提出了用反证法来解决问题4.3归结演绎推理子句：在谓词逻辑中，称原子谓词公式及其否定为文字；任何文字的析取式为子句。例如，P(x)Q(x),P(x,f(x))Q(x,g(x))都是子句。而P(x)

、Q(x,g(x))、P(x,f(x))等都是文字。并把不包含任何文字的子句称为空子句。654.3归结演绎推理子句：在谓词逻辑中，称原子谓词公式及其否定4.3归结演绎推理由于空子句不包含任何文字，它不能被任何解释所满足，所以空子句是永假的，不可满足的。由子句构成的集合称为子句集。在谓词逻辑中任何一个谓词公式均可通过等价变换化为相应的子句集。664.3归结演绎推理由于空子句不包含任何文字，它不能被任何解释4.3归结演绎推理化子句集的步骤如下：1、利用等价公式消去公式中的逻辑连接词“”和“”：PQPQPQ（PQ）（PQ）674.3归结演绎推理化子句集的步骤如下：674.3归结演绎推理2、利用下列公式将否定符号“”深入到单个变元前PP（PQ）PQ（PQ）PQ(x)P(x)P(x)P(x)P684.3归结演绎推理2、利用下列公式将否定符号“”深入到单个4.3归结演绎推理3、重新命名变元名，使不同量词约束的变元有不同的名字4、消去存在量词。分两种情况处理：一种情况是存在量词不出现在全称量词的辖域内，此时只要用一个新的个体常量替换受该存在量词约束的变元就可消去存在量词；另一种情况是存在量词位于一个或多个全称量词的辖域内，例如（x1)（x2)…(xn)(y)P(x1,x2,…,xn,y)此时需要用Skolem函数f(x1,x2,…,xn)替换受该存在量词约束的变元，然后才能消去存在量词。694.3归结演绎推理3、重新命名变元名，使不同量词约束的变元有4.3归结演绎推理5、把全称量词全部移到公式的左边。6、利用等价关系P(QR)=(PQ)(PR)把公式化为Skolem标准型。704.3归结演绎推理5、把全称量词全部移到公式的左边。70

4.3归结演绎推理Skolem标准型的一般形式是：（x1)（x2)…(xn)M其中，M是子句的合取式，称为Skolem标准型的母式。7、消去全称量词8、对变元更名，使不同子句中的变元不同名。714.3归结演绎推理Skolem标准型的一般形式是：714.3归结演绎推理9、消去合取连接词，变为子句集。子句集中各子句之间是合取关系。谓词公式是不可满足的，则其子句集合是不可满足的，反之亦然。724.3归结演绎推理9、消去合取连接词，变为子句集。子句集中各

海伯伦理论如何证明一个子句集是不可满足的呢？下面就海伯伦理论和鲁宾逊的归结原理进行讨论。一、海伯伦理论要判定一个子句集是否是不可满足的，需要对子句集中的谓词公式进行判定，而谓词公式的判定需要对个体域上的任何解释进行判定，这是很困难的。73海伯伦理论如何证明一个子句集是不可满足的呢？下面就海伯伦理

海伯伦理论海伯伦定义了一个特殊的域称为海伯伦域，在任何域上的判定，只要在海伯伦域上进行即可。*设S是子句集，则按下述方法构造的域H称为是海伯伦域：74海伯伦理论海伯伦定义了一个特殊的域称为海伯伦域，在任何域

海伯伦理论1、令H0是S中所有个体常量的集合，若S中不包含个体常量，则令H0={a}，其中a为任意指定的一个个体常量。2、令Hi+1=Hi{S中所有n元函数f(x1,x2,…,xn)|xj(j=1,2,…,n)是Hi中的元素}，其中，i=0,1,…。下面通过例子来解释这个定义。

75海伯伦理论1、令H0是S中所有个体常量的集合，若S中不包含海伯伦理论例1求子句集S={P(x)Q(x),R(f(y))}的H域。解：因为S中没有个体常量，所以指定a作为个体常量，于是得到：H0={a},H1={a,f(a)},H2={a,f(a),f(f(a))},H３={a,f(a),f(f(a))，f(f(f(a)))},H={a,f(a),f(f(a)),…}76海伯伦理论例1求子句集S={P(x)Q(x),R(f(y)海伯伦理论例2求子句集S={P(a),Q(b),R(f(x))}的H域解：根据H域的定义得到：H0={a,b}H1={a,b,f(a),f(b)}H2={a,b,f(a),f(b),f(f(a)),f(f(b))}┇77海伯伦理论例2求子句集S={P(a),Q(b),R(f(x海伯伦理论例3：求子句集S={P(x),Q(y)R(y)}的H域。解：由于该子句集中既无个体常量，又无函数，所以可任意指定一个常量a作为个体常量，从而得到H0=H1=…=H={a}有定理说：子句集S是不可满足的充要条件是S对H域上的一切解释都为假。并且海伯伦证明了若子句集S在任何域D上的解释能满足S，则在H域上相应的解释也能满足S。下面我们说明，S在H域上解释的定义：78海伯伦理论例3：求子句集S={P(x),Q(y)R(y)}海伯伦理论子句集S在H域上的一个解释满足下列条件：1、在解释I下，常量映射到自身；2、S中的任一个n元函数是HnH的映射。即，设h1,h2,…,hnH,则f(h1,h2,…,hn)H;79海伯伦理论子句集S在H域上的一个解释满足下列条件：79海伯伦理论3、S中的任一n元谓词是Hn{T，F}的映射。即谓词的真值可以指派T也可指派F。海伯伦在理论上证明了子句集不可满足性的可行性及方法，但要在计算机上实现其证明过程还是很困难的。1965年鲁宾逊提出了归结原理，使机器证明成为现实80海伯伦理论3、S中的任一n元谓词是Hn{T，F}的映射。即鲁宾逊归结原理归结原理也称消解原理，是鲁宾逊提出的一种证明子句不可满足性，从而实现定理证明的一种理论及方法。由谓词公式转化为子句集的过程可以看出，在子句集中子句之间的关系是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。前面，我们曾经说过空子句是不可满足的，即一个子句集中若含空子句，则它是不可满足的。81鲁宾逊归结原理归结原理也称消解原理，是鲁宾逊提出的一种证明子鲁宾逊归结原理归结原理的基本思想就是检查子句集中是否含空子句，若含，则子句集S不可满足，或说证明一个谓词公式是永假的过程，就是归结由此公式转换成的子句集包含空子句的过程。82鲁宾逊归结原理82鲁宾逊归结原理下面我们先来说明命题逻辑中的归结原理定义P是原子谓词公式，则称P与P为互补文字。我们知道在命题逻辑中有公式：PQ,QRPR即PQ，QRPRc1c2c1283鲁宾逊归结原理下面我们先来说明命题逻辑中的归结原理83鲁宾逊归结原理显然上述公式向我们展示的是在子句c1

中存在文字Q，在子句c2中存在Q的补文字Q，把这一对互补文字消去，剩下的文字析取起来就是子句

c1和c2的逻辑结果c12。并称c12是c1和c2的归结式，c1和c2则称为c12的亲本子句。84鲁宾逊归结原理显然上述公式向我们展示的是在子句c1中存在文鲁宾逊归结原理例如：1、C1=PQRC2=QS它们的归结式c12为PRS2、C1=PC2=P它们的归结式c12为NIL即空子句。85鲁宾逊归结原理例如：85鲁宾逊归结原理3、C1=PQC2=QRC3=P它们的归结式c123为R。其归结过程可以用下面的一个树形结构很清楚的表现出来。86鲁宾逊归结原理3、C1=PQ86鲁宾逊归结原理

PQQRPRPR

归结过程的树形表示图

87鲁宾逊归结原理鲁宾逊归结原理由命题逻辑中的归结原理可以得出如下的推论：设c1与c2是子句集S中的两个子句，c12是它们的归结式,若用c12代替c1和c2后得到新子句集S1，则由S1的不可满足性可以推出S的不可满足性。这个定理告诉我们，证明子句集S的不可满足性问题，可以转化成证子句集S1的不可满足性问，…直到从子句集Sn

中推出一个空子句来。88鲁宾逊归结原理由命题逻辑中的归结原理可以得出如下的推论：88鲁宾逊归结原理在谓词逻辑中，由于子句中含有变元，所以不象命题逻辑中那样可以直接消去互补文字，而先要用最一般合一对变元进行代换。然后才能进行归结。前面我们已经介绍过最一般合一的概念，下面给出谓词逻辑中二元归结式的概念。89鲁宾逊归结原理在谓词逻辑中，由于子句中含有变元，所以不象命题鲁宾逊归结原理设C1与C2是两个没有公共变量的子句，L1和L2分别是C1与C2中的文字，若是L1和L2的最一般合一，则称C12=（C1-{L1}）（C2-{L2}）为C1与C2的二元归结式，L1和L2称为归结式上的文字。例子见P132页的例4.10和例4.11。90鲁宾逊归结原理设C1与C2是两个没有公共变量的子句，L1和L鲁宾逊归结原理

例如设

C1=P(a)Q(x)R(x)

C2=P(y)Q(b)若选L1=P(a),L2=P(y),则={a/y}是L1

与

L2的最一般合一．于是有C12=(C1-{L1})(C2-{L2})

={Q(x)R(x)}{Q(b)}

={Q(x),R(x),Q(b)}.

91鲁宾逊归结原理例如设

C1=P(a)Q(x)R(鲁宾逊归结原理

若选L1=Q(x),L2=Q(b),则={b/x}是L1

与

L2的最一般合一．于是有C12=(C1-{L1})(C2-{L2})

={Q(x)R(x)}{Q(b)}

={P(a),R(b),P(y)}.92鲁宾逊归结原理若选L1=Q(x),L2=Q(b)鲁宾逊归结原理再例如设有如下子句：Ｃ1=P(x)Q(a),Ｃ2=P(b)R(x)由于Ｃ1和Ｃ2

有相同的变元不符合二元归结式中定义中对子句Ｃ1和Ｃ2的要求．为了归结的需要，要修改Ｃ2中变元的名字．

93鲁宾逊归结原理再例如设有如下子句：93鲁宾逊归结原理令Ｃ2=P(b)R(y),此时，Ｌ1=P(x),Ｌ2=P(b),它们的最一般合一为＝｛b/x｝.于是有C12=({P(b),Q(a)}–{P(b),})({P(b)R(y),}-{P(b)})={Q(a),R(y)}.如果在参加归结的子句内部有可合一的文字，则在归结之前应先对这些文字合一，见下例：94鲁宾逊归结原理令Ｃ2=P(b)R(y),此时，Ｌ1=P(鲁宾逊归结原理设有子句：C1=P(x)P(f(a))Q(x)C2=P(y)R(b)由于在C1中有可合一文字P(x)和P(f(a))，若用它们的最一般合一＝{f(a)/x｝进行代换，得到

C1=P(f(a))Q(f(a))此时可对C1和C2进行归结，从而的到C1和C2的二元归结式．对C1和C2分别选Ｌ1=P(f(a)),Ｌ2=P(y),它们的最一般合一是95鲁宾逊归结原理设有子句：C1=P(x)P(f(a))鲁宾逊归结原理＝｛f(a)/y｝于是可得它们的归结式为：C12＝Ｒ(b)Q(f(a))上例中称C1为C1因子，如果C1是一个单文字，则称它为C1的单元因子．应用因子的概念，可对谓词逻辑中的归结原理给出如下的定义．96鲁宾逊归结原理＝｛f(a)/y｝于是可得它们的归结式为：9鲁宾逊归结原理定义；子句Ｃ1和Ｃ２的归结式是下列二元归结式之一：(1)Ｃ1和Ｃ２的二元归结式；(2)Ｃ1和Ｃ２的因子Ｃ２2的二元归结式；(3)Ｃ１的因子Ｃ11和Ｃ２的二元归结式；(4)Ｃ1的因子Ｃ11和Ｃ２的因子Ｃ２2的二元归结式；97鲁宾逊归结原理定义；子句Ｃ1和Ｃ２的归结式是下列二元归结式之鲁宾逊归结原理在谓词逻辑中仍然有，归结式是它的亲本子句的逻辑结果，用归结式代替子句集Ｓ中的亲本子句所得到的新子句集Ｓ仍然保持子句集Ｓ的不可满足性．98鲁宾逊归结原理在谓词逻辑中仍然有，归结式是它的亲本子句的逻辑归结反演归结反演原理：欲证P1,P2,,PnQ(1)P1P2,,PnQ＝T(2)(P1P2,,Pn)Q＝T(3)(P1P2,,Pn)Q＝F(4)我们的工作过程是从后向前进行的，即证(4)就是证明了(3),证(3)就是证明了(2),证(2)就是证明了(1)．99归结反演归结反演原理：欲证99归结反演在使用消解过程之前，我们必须把任一谓词公式转换成子句，下面给出转化过程的步骤：（1）消去单条件运算符号“”，应用公式AB=AB（2）将否定符号深入到单个谓词变元的前面，利用公式（AB）=AB（AB）=AB((x)A(x))=(x)A(x)((x)A(x))=(x)A(x)

100归结反演在使用消解过程之前，我们必须把任一谓词公式转换成子句归结反演(3)对变量标准化在任一量词辖域内，受该量词约束的变量为一哑元（虚构变量），它可以在该辖域内处处统一地被另一个没有出现过的任一变量所代替，而不改变公式的真值。合适公式中变量的标准化意味着对哑元改名以保证每个量词有其自己唯一的哑元。例如把(x)（A(x)(x)（B（x）））标准化为(x)（A(x)(y)（B（y）））101归结反演(3)对变量标准化101归结反演(4)消去存在量词在公式(x)((y)P(x,y))中，存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依赖关系明显地由函数g（y）所定义，它把每个y值映射到存在的那个x。这种函数叫做skolem函数。如果用skolem函数代替存在的x，我们就可以消去全部存在量词，并写成(y)(P(g(y),y))102归结反演(4)消去存在量词102归结反演在公式(x)((y)P(x,y))中，存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依赖关系明显地由函数g（y）所定义，它把每个y值映射到存在的那个x。这种函数叫做skolem函数。如果用skolem函数代替存在的x，我们就可以消去全部存在量词，并写成(y)(P(g(y),y))103归结反演在公式(x)((y)P(x,y))中，存在归结反演从一个公式消去存在量词的一般规则是以一个skolem函数代替每个出现的存在量词的量化变量，而这个skolem函数的变量就是由那些全称量词所约束的全称量词量化变量，这些全称量词的辖域包括要被消去的存在量词的辖域在内。skolem函数所使用的函数符号必须是新的，即不允许是公式中已经出现过的函数符号。例如：(y)(x)P(x,y)被(y)(P(g(y),y))代替，其中g(y)为一skolem函数。104归结反演从一个公式消去存在量词的一般规则是以一个skolem归结反演如果要消去的存在量词不在任何一个全称量词的辖域内，那麽我们就用不含变量的skolem函数即常量。例如，(x)P(x)化为P(A)，其中常量符号A用来表示我们知道的存在实体。A必须是个新的常量符号，它未曾在公式中其它地方使用过。105归结反演如果要消去的存在量词不在任何一个全称量词的辖域内，那归结反演（5）化为前束形到这一步已不留下任何存在量词，而且，每个全称量词都有自己的变量。把所有全称量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。所得公式称为前束形。106归结反演（5）化为前束形106归结反演前束形公式由前缀和母式组成，前缀由全称量词组成，母式由没有量词的公式组成，即前束形=（前缀）（母式）全称量词串无量词公式107归结反演前束形公式由前缀和母式组成，前缀由全称量词组成，母式归结反演（6）把母式化为合取范式任何母式都可写成由一些谓词公式和（或）谓词公式的否定的析取的有限集组成的合取。这种母式叫做合取范式。我们可以反复应用对的分配律，把任一母式化成合取范式。例如，A（BC）=（AB）（AC）108归结反演（6）把母式化为合取范式108归结反演（7）消去全称量词到了这一步，所有余下的量词均被全称量词量化了。同时，全称量词的次序已经不重要了。于是我们可以消去全称量词。109归结反演（7）消去全称量词109归结反演（8）消去连接词符号，用A，B代替AB。这样反复代替的结果，最后得到一个有限集，其中每个公式是文字的析取。任一个只由文字的析取构成的合式公式叫做一个子句。（9）更换变量名称可以更换变量符号的名称，使一个变量符号不出现在一个以上的子句中。下面我们用例子来说明化子句并进行消解的过程：110归结反演（8）消去连接词符号，用A，B代替AB。这样反复归结反演例1试证：G是F1和F2的逻辑结论，其中F1：(x)(P(x)(y)(Q(y)L(x,y)))F2：(x)(P(x)(y)(R(y)L(x,y)))G：

(x)(R(x)Q(x))(x)(P(x)(y)(Q(y)L(x,y))),(x)(P(x)(y)(R(y)L(x,y)))(x)(R(x)Q(x))111归结反演例1试证：G是F1和F2的逻辑结论，其中111归结反演证明：首先把F1

，F2

和G转化成子句形：F1=(x)(P(x)(y)(Q(y)L(x,y)))=(x)(P(x)(y)(Q(y)

L(x,y)))=(x)(y)(P(x)

Q(y)

L(x,y))=P(x)

Q(y)

L(x,y).112归结反演证明：首先把F1，F2和G转化成子句形：112归结反演F2=(x)(P(x)(y)(R(y)L(x,y)))=(x)(P(x)(y)(R(y)

L(x,y))=(P(a)(y)(R(y)

L(a,y))=(y)(P(a)(R(y)

L(a,y))P(a),R(z)

L(a,z)113归结反演F2=(x)(P(x)(y)(R(y)归结反演G=(x)(R(x)Q(x))=(x)(R(x)

Q(x)=(R(x)Q(x))R(b),Q(b)得到子句集合如下：1.P(x)

Q(y)

L(x,y)2.P(a)3.R(z)

L(a,z)S4.R(b)5.Q(b)114归结反演G=(x)(R(x)Q(x))11归结反演6.Q(y)

L(a,y)1和2及a/x7.L(a,b)5和6及b/y8.R(b)3和7及b/z9.4和8及

=即S是不可满足的，G是F1和F2的逻辑结论。115归结反演6.Q(y)L(a,y)1和2归结反演例2、已知：任何人的兄弟不是女性，任何人的姐妹必是女性，Mary是Bill的姐妹，试用归结推理的方法证明Mary不是Tom的兄弟。解：为了求解此问题首先定义如下谓词：brother(x,y):x是y的兄弟；sister(x,y):x是y的姐妹；woman(x):x是女性。116归结反演例2、已知：任何人的兄弟不是女性，任何人的姐妹必是女归结反演于是问题可以描述成：(x)(y)(brother(x,y)woman(x)),(x)(y)(sister(x,y)woman(x)),sister(Mary,Bill)

brother(Mary,Tom)117归结反演于是问题可以描述成：117归结反演首先将前提和结论的否定转换成子句形:(x)(y)(brother(x,y)woman(x))=brother(x,y)

woman(x);(x)(y)(sister(x,y)woman(x))=

sister(x,y)woman(x);brother(Mary,Tom)=brother(Mary,Tom);sister(Mary,Bill).118归结反演首先将前提和结论的否定转换成子句形:118归结反演整理得子句集合S如下：1、sister(Mary,Bill)2、brother(Mary,Tom)S3、brother(x,y)woman(x)4、

sister(z,w)woman(z)119归结反演整理得子句集合S如下：119归结反演5、woman(Mary)和3及Mary/x,Tom/y

6、woman(Mary)1和4及Mary/z,Bill/w7、

5和6及空代换

问题得证.120归结反演5、woman(Mary)和3及Mary/x,T归结反演例3、已知，John是贼。Paul喜欢酒（wine）,Paul也喜欢奶酪（cheese）。如果Paul喜欢某物则John也喜欢某物。如果某人是贼，并且他喜欢某物，则他很可能会偷窃该物。试用归结推理的方法证明John可能偷窃了什麽？121归结反演例3、已知，John是贼。Paul喜欢酒（wine）归结反演解：为了求解该问题定义如下谓词：thief(x):x是贼like(x,y):某人x喜欢某物ymay-steal(x,y):某人x可能偷窃了某物y122归结反演解：为了求解该问题定义如下谓词：122归结反演于是问题可以描述成：thief(John)，like(Paul，wine)，like(Paul，cheese)，(y)(like(Paul,y)like(John,y)),(x)(thief(x)(y)(like(x,y)may-steal(x,y)))may-steal(John,Z).123归结反演于是问题可以描述成：123归结反演首先把前提和结论的否定转换成子句形：(y)(like(Paul,y)like(John，y))=like(Paul，y)like(John，y);(x)(thief(x)(y)(like(x,y)may-steal(x,y))=thief(John)(y)(like(John,y)

may-teal(John,y))=(y)(thief(John)(like(John,y)may-steal(John,y))）=thief(John)(like(John,y)may-steal(John,y)).124归结反演首先把前提和结论的否定转换成子句形：124may-steal(John,Z).整理得子句集合S为：1、thief(John)2、like(John,y)may-steal(John,y)3、like(Paul,wine)4、like(Paul,cheese)5、may-steal(John,Z)6、like(Paul，X)like(John，X)7、like(John,wine)3和6及wine/x8、may-steal(John,wine)2和7及wine/y9、

5和8及

问题得证。125may-steal(John,Z).125应用归结原理求取问题的答案利用归结原理还可以来求取问题的答案，思想与定理证明类似．其求解步骤如下：１、把已知前提用谓词公式表示出来，并且化为相应的子句集Ｓ；２、把待求解的问题也用谓词公式表示出来，然后把它否定并与谓词ANSWER构成析取式，ANSWER是一个为了求解问题而专设的谓词，其变元必须与待求解问题公式的变元完全一致；126应用归结原理求取问题的答案利用归结原理还可以来求取问题的答案应用归结原理求取问题的答案３、把析取式化为子句集，并且把该子句并入到子句集Ｓ中，得到子句集合Ｓ；４、对Ｓ应用归结原理进行归结；５、若得到归结式ANSWER，则答案就在ANSWER中。127应用归结原理求取问题的答案３、把析取式化为子句集，并且把该子应用归结原理求取问题的答案例：Ｆ1:已知王（wang)先生是小李(li)的老师.Ｆ2:小李与小张(zhang)是同班同学．Ｆ3:如果x与y是同班同学，则x的老师也是y的老师．求小张的老师是谁？128应用归结原理求取问题的答案例：128应用归结原理求取问题的答案解：首先定义谓词：T(x,y):x是y的老师．C(x,y):x与y是同班同学．把已知前提和待求解的问题表示成谓词公式：F1:T(wang,li)F2:C(li,zhang)F3:(x)(y)(z)(C(x,y)T(z,x)T(z,y)).129应用归结原理求取问题的答案解：首先定义谓词：129应用归结原理求取问题的答案G:(x)T(x,zhang)ANSWER(x)把上述公式化为子句集：（1）T(wang,li)（2）C(li,zhang)S（3）

C(x,y)

T(z,x)T(z,y).(4)T(u,zhang)ANSWER(u)130应用归结原理求取问题的答案G:(x)T(x,zhang)应用归结原理求取问题的答案应用归结原理进行归结：(5)C(li,y)T(z,y).(1)和(3)归结(6)C(li,zhang)ANSWER(wang)(4),(5)(7)ANSWER(wang)(2)与(6)归结其归结树如Ｐ137的图４-9所示

131应用归结原理求取问题的答案应用归结原理进行归结：131应用归结原理求取问题的答案例：设Ａ,B,C三人中有人从不说真话，也有人从不说假话，某人向这三人分别提出同一个问题：谁是说谎者？Ａ答：“Ｂ和Ｃ是说谎者”；Ｂ答：“Ａ和Ｃ是说谎者”；Ｃ答：“Ａ和Ｂ中至少有一个说谎者”．求谁是诚实的人，谁是说谎者？132应用归结原理求取问题的答案例：设Ａ,B,C三人中有人从不说真应用归结原理求取问题的答案解：令T(x):表示x说真话如果Ａ说的是真话，则有T(A)T(B)T(C)如果Ａ说的是假话，则有T(A)(T(B)T(C))对Ｂ和Ｃ说的话做相同的处理得：

T(Ｂ)T(Ａ)T(C)T(Ｂ)(T(Ａ)T(C))133应用归结原理求取问题的答案解：令T(x):表示x说真话133应用归结原理求取问题的答案T(Ｃ)(T(Ａ)T(B))T(C)(T(Ａ)T(B))把上面的公式化为子句集Ｓ得：(1)T(Ａ)T(B)(2)T(Ａ)T(C)(3)T(B)T(C)(4)T(Ｂ)T(Ａ)T(C)(5)T(Ｃ)T(Ａ)T(B)(6)T(Ａ)T(C)

134应用归结原理求取问题的答案T(Ｃ)(T(Ａ)T(应用归结原理求取问题的答案(7)T(B)T(C)下面首先求谁是老实人．把T(x)ANSWER(x)并入Ｓ得Ｓ1(8)T(x)ANSWER(x)在Ｓ1上进行归结得(9)T(A)T(C)(1)和(7)

135应用归结原理求取问题的答案(7)T(B)T(C)13应用归结原理求取问题的答案(10)T(C)(6)和(9)(11)ANSWER(C)(8)和(10)及{C/x}即Ｃ是老实人．由于对Ｓ1进行归结得不出ANSWER(Ｂ)和ANSWER(Ａ)．所以下面来证明Ａ和Ｂ不是老实人．设Ａ不是老实人，则有T(Ａ)把它的否定并入Ｓ中得Ｓ2

136应用归结原理求取问题的答案(10)T(C)(6应用归结原理求取问题的答案即Ｓ2只比Ｓ多了一个子句(8)(T(Ａ))(9)T(Ａ)T(C)(1)和(7)(10)T(Ａ)(2)和(9)(11)NIL(8)和(10)所以Ａ不是老实人，同理可证Ｂ不是老实人．137应用归结原理求取问题的答案即Ｓ2只比Ｓ多了一个子句137归结策略实际用计算机进行归结时使用的是水平浸透法，即对Ｓ中的每一对子句进行比较，有归结式即产生直到推出一个空子句．从上面的例子我们可以看出影响归结效率的重要因素是子句的数量和子句中文字的数量．下面我们给出一些提高归结效率的方法．138归结策略实际用计算机进行归结时使用的是水平浸透法，即对Ｓ中的归结策略要想提高消解效率，当然是希望子句集合S中的子句越少越好，子句中的文字越少越好。为了提高消解效率，人们提出了很多控制策略，例如：删除策略，线性归结，单元归结，输入归结等。139归结策略要想提高消解效率，当然是希望子句集合S中的子句越少越删除策略所谓删除策略是指，若子句集合S中有永真式则直接可以删除，因为它不影响子句集合S的不可满足性，此外被前面子句归类的子句也可以被删除。下面给出归类的概念：设有两个子句C和D，若有置换（或代换），使得C

D成立，便说子句C把子句D归类，或说D被C归类，于是子句D可以从S中删除。140删除策略所谓删除策略是指，若子句集合S中有永真式则直接可以删删除策略其中：C表示子句C在代换下的例式，即将子句C中的变元用中的项代换所得的结果。例如C=p(x)D=p(a)Q(a)取=a/x于是有C=p(a)于是有

p(a)p(a)，Q(a)

其中逗号代表的是析取。141删除策略其中：C表示子句C在代换下的例式，即将子句C中的删除策略设子句序列C1，C2，，Ck是从S推出Ck的演绎，若在演绎的过程中随时删除永真公式和被前面归类的子句，就称在这个演绎的过程中实行了删除策略。删除策略是完备的，即对于不可满足的子句集合S来说，如果在水平浸透法中使用删除策略，那麽一定存在一个空子句Sn。142删除策略设子句序列C1，C2，，Ck是从S推出Ck的演绎，删除策略下面给出归类算法（SubsumptionAlgorithm）设D=L1L2Lm,有

=a1/x1,a2/x2,,an/xn,其中x1

，x2，，xn是D中所有变元的符号,a1,a2,,an是C和D中都没有的互不相同的常量符号。步1

令W=

L1

，

,Lm

,K=0,U0=C;步2

若

Uk则算法停，C归类D。步3

令Uk+1=R(C1,C2)C1Uk,C2

W;步4

若Uk+1=，则算法停，C不归类D。步5

令K=K+1,转步2143删除策略下面给出归类算法（SubsumptionAlgor删除策略由于U0

，U1，

,Uk，序列中，后一个子句集中的每一个子句一定比前一个子句集中的亲本子句少一个文字，而子句中的文字是有限的，所以，最后一定存在一个n使Uk=或

Un即算法是可停的.本算法是完备的，即子句C归类子句D，当且仅当归类算法停在步2。144删除策略由于U0，U1，,Uk，序列中，后一个子句删除策略例如给定

C=P（x）Q(f(x),a)D=P（h(y)）

Q(f(h(y)),a)P(z)试判定C是否可归类D？解：令

=b/y,c/zW=P（h(b)）,Q(f(h(b)),a),P(c),K=0U0=P（x）Q(f(x),a)K=0:因

U0145删除策略例如给定145删除策略U1=Q(f(h(b),a),P(h(b)),Q(f(c),