《人工智能》第三章知识演绎

主讲：夏幼明《人工智能》示范课程2①规章演绎系统②谓词演绎的归结方法③归结反对搜寻策略④Hone子句的归结“学问演绎”核心内容3规章演绎系统在基于规章系统中，每个if可能与某断言(assertion)集中的一个或多个断言匹配；then局部用于规定放入工作内存的新断言。这种系统叫做基于规章的演绎系统(rulebaseddeductionsystem)。在这种系统中，通常称规章的if局部为前项(antecedent)，称规章的then局部为后项(consequent)。4规章演绎系统基于规章的求解系统由if-then形式的规章建立的。例如：if(antecedent)then(consequent)

基于规章的系统称为规章演绎系统，假设后件用于规定动作，则称为产生式系统。规章演绎系统可以分为如下的3种：规章正向演绎系统、规章逆向演绎系统、规章双向演绎系统。

前件

后件5规章演绎系统(1)规章正向演绎系统从if局部向then局部推理的过程称为正向推理，即从事实或状态向目标或行动进展操作。 规章正向演绎系统的步骤：事实表达命题式的与或形变换利用(W1→W2)和(W1∨W2)的等价关系，消去符号→(假设存在该符号的话)。实际上，在事实中间很少有符号→消失，由于可把蕴涵式表示为规章。用狄·摩根(DeMorgan)定律把否认符号移进括号内，直到每个否认符号的辖域最多只含有一个谓词为止。

6规章演绎系统(1)规章正向演绎系统从if局部向then局部推理的过程称为正向推理，即从事实或状态向目标或行动进展操作。 规章正向演绎系统的步骤：xyP(x,y)事实表达命题式的与或形变换xP(x,f(x))yxP(x,y)xP(x,a)~xP(x)x~P(x)对所得到的表达式进展Skolem化和前束化。对全称量词辖域内的变量进展改名和变量标准化，而存在量词量化变量用Skolem函数代替。删去全称量词，而任何余下的变量都被认为具有全称量化作用。7规章演绎系统(1)规章正向演绎系统从if局部向then局部推理的过程称为正向推理，即从事实或状态向目标或行动进展操作。 规章正向演绎系统的步骤：例1：我们有事实表达式(u)(v){Q(v，u)∧[(R(v)∨P(v))∧S(u，v)]}把它化为：Q(v,A)∧{[R(v)∧P(v)]∨S(A,v)}对变量更名标准化，使得同一变量不消失在事实表达式的不同主要合取式中。更名后得表达式：Q(w,A)∧{[R(v)∧P(v)]∨S(A,v)}必需留意到Q(v，A)中的变量v可用新变量w代替，而合取式[R(v)∧P(v)]中的变量v却不行更名，由于后者也消失在析取式S(A,v)中。8规章演绎系统(1)规章正向演绎系统从if局部向then局部推理的过程称为正向推理，即从事实或状态向目标或行动进展操作。 规章正向演绎系统的步骤：例2：我们有事实表达式(v)(u){Q(v，u)∧[(R(v)∨P(v))∧S(u，v)]}留意，这时变量u成为了变量v的函数f(v)，利用Skolem函数把这个表达式化为：Q(v,f(v))∧{[R(v)∧P(v)]∨S(f(v),v)}9规章演绎系统(1)规章正向演绎系统 规章正向演绎系统的步骤：事实表达命题式的与或形变换R(V)P(V)

R(V)∧P(V)S(A,V)[R(V)∧

P(V)]∨S(A,V)Q(W,A)Q(W,A)∧{[R(V)∧P(V)]∨S(A,V)}

每个节点表示该事实表达式的一个子表达式。某个事实表达式(E1∧…∧En)的每个合取子表达式E1，…，En是用后继节点表示的，并由一个k线连接符把它们连接到父辈节点上。某个事实表达式(E1∨…∨Ek)的析取关系子表达式E1，…，Ek是由单一的后继节点表示的，并由一个单线连接符接到父辈结点。10规章演绎系统(1)规章正向演绎系统 与或图的正向推理：限制规章的公式类型为：LW 其中：L为单文字；W为与或形的唯一公式。例如：考虑规章S(x∧y)∨z应用到右面的事实表达式中。TS(T∨U)[S∧(T∨U)][(P∨Q)∧R]∨[S∧(T∨U)](P∨Q)RPQU[(P∨Q)∧R]表示某个事实表达式的与或图的叶节点均由表达式中的文字来标记。图中标记有整个事实表达式的节点，称为根节点，它在图中没有祖先。XYSX∧YZ当目标公式按正向规章应用到事实表达式与或图，产生的与或图包含有终止在目标节点的一个解图时，证明目标公式成立。11规章演绎系统(1)规章正向演绎系统 与或图的正向推理：公式的与或图表示有个好玩的性质，即由变换该公式得到的子句集可作为此与或图的解图的集合(终止于叶节点)读出；也就是说，所得到的每个子句是作为解图的各个叶节点上文字的析取。这样，由表达式Q(w,A)∧{[R(v)∧P(v)]∨S(A,v)}得到的子句为：Q(w,A),S(A,v)∨R(v),S(A,v)∨P(v)我们一般把事实表达式的与或图表示倒过来画，即把根节点画在最下面，而把其后继节点往上画。我们将要争论到目标公式的与或图表示，它是按通常方式画出的，即目标在上面。

12规章演绎系统(1)规章正向演绎系统 推理规章：消解(归结)把原子公式和原子公式的否认称为文字。任何文字的析取式称为子句。析取式P⋁Q⋁¬R可用子句表示为：{P，Q，¬R}。不包含任何文字的子句称为空子句〔NIL〕。空子句是永假的。由子句构成的集合称为子句集。归结定义为：从{}1和{}2(1和2是文字集合，是一个文字)，可以归结为12，它被称为两个子句的归结式。是被归结的文字。这个过程称为归结。13规章演绎系统(1)规章正向演绎系统 推理规章：消解(归结)归结定义为：从{}1和{}2(1和2是文字集合，是一个文字)，可以归结为12，它被称为两个子句的归结式。是被归结的文字。这个过程称为归结。例：1、P⋁R和Q⋁¬R归结R为P⋁Q。留意到P⋁R与Q⋁¬R的等价写法为¬P⊃R、R⊃Q，利用蕴涵“⊃”的传递性，则有¬P⊃Q，而它的等价表示为P⋁Q。于是，可以看出，通过链式的推理规章产生的结果与归结是全都的。2、R和Q⋁¬R归结R为Q。而Q⋁¬R等价于R⊃Q，这样，此归结与假言推理是全都的。14规章演绎系统(1)规章正向演绎系统 推理规章：消解(归结)归结是合理的。证明：所谓合理的，就是说，假设{}1和{}2均是真的，那么12是真的。对的真假值争论就可以了。情形一：是真的，那么，是假的，因此，{}2为真，必需2为真，故12是真的。情形二：是假的，那么，{}1为真，必需1为真，故12是真的。综合情形一和二，可知，1、2至少有一个必需为真，即12是真的。15规章演绎系统(1)规章正向演绎系统 与或图的正向推理：应用消解原理的结果:规章S→(X∧Y)∨Z化为子句： S∨X∨Z；S∨Y∨Z；事实表达式[(P∨Q)∧R]∨[S∧(T∨U)]化为 子句：P∨Q∨S；R∨S；P∨Q∨T∨U；R∨T∨U归结结果：X∨Z∨P∨Q；Y∨Z∨P∨Q； R∨X∨Z；R∨Y∨Z16规章演绎系统(1)规章正向演绎系统 与或图的正向推理：应用一条规章得到的与或图连续表示事实表达式和推得的表达式，这可利用匹配弧两侧有一样标记的节点来实现。对一个节点应用一条规章之后，此节点就不再是该图的叶节点。不过，它仍旧由单一文字标记而且可以连续具有一些应用于它的规章。我们把图中标有单文字的任一节点都称为文字节点，由一个与或图表示的子句集就是对应于该图中以文字节点终止的解图集。17规章演绎系统(1)规章正向演绎系统 作为终止条件的目标公式应用规章推理的目的在于从某个事实公式和某个规章集动身来证明某个目标公式。在正向推理系统中，这种目标表达式只限于可证明的表达式，尤其是可证明的文字析取形的目标公式表达式。我们用文字集表示此目标公式，并设该集各元都为析取形式。目标文字和规章可用来对与或图添加后继节点，当一个目标文字与该图中文字节点n上的一个文字相匹配时，我们就对该图添加这个节点n的新后裔，并标记为匹配的目标文字。这个后裔叫做目标节点，目标节点都用匹配弧分别接到它们的父辈节点上。18规章演绎系统(1)规章正向演绎系统 作为终止条件的目标公式例3：事实P∨Q；规章P→C，Q→G；目标C∨G。把规章化为子句形，得子句集：P∨C，Q∨G

目标的否认为:(C∨G)；其子句形为:C，GP∨

CP∨

QQ∨

CCQ

Q∨

G

G

Q

NIL19规章演绎系统(1)规章正向演绎系统 作为终止条件的目标公式例3：事实P∨Q；规章P→C，Q→G；目标C∨G。PQPR(P∨Q)[(P∨O)∧R][S∧(T∨U)]∨[(P∨Q)∧R](T∨U)STUQ[(T∨U)∧S]CDEGCG当目标公式按正向规则应用到事实表达式与或图，产生的与或图包含有终止在目标节点的一个解图时，证明目标公式成立。20规章演绎系统(2)规章逆向演绎系统基于规章的逆向演绎系统，其操作过程与正向演绎系统相反，即为从目标到事实的操作过程，从then到if的推理过程。 目标表达式的与或形式承受与变换事实表达式同样的过程，把目标公式化成与或形，即消去蕴涵符号，把否认符号移进括号内，对全称量词Skolem化并删去存在量词。留在目标表达式与或形中的变量假定都已存在量词量化。例1：目标表达式：(y)(x){P(x)→[Ｑ(x,y)∧[P(x)∧S(y)]]}

被化成与或形：P(f(y))∨{Q(f(y),y)∧[P(f(y))∨S(y)]}

式中，x=f(y)为一Skolem函数。21规章演绎系统(2)规章逆向演绎系统目标表达式的与或形式与或形的目标公式也可以表示为与或图。不过，与事实表达式的与或图不同的是，对于目标表达式，与或图中的k线连接符用来分开合取关系的子表达式。在目标公式的与或图中，我们把根节点的任一后裔叫做子目标节点，而标在这些后裔节点中的表达式叫做子目标。例1：目标表达式：P(f(y))∨{Q(f(y),y)∧[P(f(y))∨S(y)]}P(f(y))∨{Q(f(y),y)∧[P(f(y))∨S(y)]}Q(f(y),y)

∧[P(f(y))∨S(y)]P(f(y))Q(f(y),y)S(y)P(f(y))P(f(y))∨S(y)22规章演绎系统(2)规章逆向演绎系统与或图的逆向推理规章变换我们应用逆向推理规章来变换逆向演绎系统的与或图构造，逆向推理规章是建立在确定的蕴涵式根底上的，现在把这些逆向推理规章限制为:W→L其中：W为任一与或形公式，L为单文字。逆向系统中的事实表达式均限制为文字合取形，它可以表示为一个文字集。当一个事实文字和标在该图文字节点上的文字相匹配时，就可把相应的后裔事实节点添加到该与或图中去。这个事实节点通过标有mgu的匹配弧与匹配的子目标文字节点连接起来。同一个事实文字可以屡次重复使用(每次用不同变量)，以便建立多重事实节点。23规章演绎系统(2)规章逆向演绎系统与或图的逆向推理规章变换事实:F1:DOG(FIDO);狗的名字叫FidoF2:BARKS(FIDO);Fido是不叫的F3:WAGS-TAIL(FIDO);Fido摇尾巴

F4:MEOWS(MYRTLE);猫咪的名字叫Myrtle

规章:R1:[WAGS-TAIL(x1)∧DOG(x1)]→FRIENDLY(x1)摇尾巴的狗是温存的狗24规章演绎系统(2)规章逆向演绎系统与或图的逆向推理规章变换规章:R2:FRIENDLY(x2)∧BARKS(x2)→AFRAID(y2,x2)温存而又不叫的东西是不值得可怕的R3:DOG(x3)→ANIMAL(x3)狗为动物

R4:CAT(x4)→ANIMAL(x4)猫为动物R5:MEOWS(x5)→CAT(x5)猫咪是猫目标:(x)(y)[CAT(x)∧DOG(y)∧AFRAID(x,y)]是否存在这样的一只猫和一条狗，使得这只猫不怕这条狗?25规章演绎系统(2)规章逆向演绎系统与或图的逆向推理规章变换CAT(x)∧DOG(y)∧AFRAID(x,y)CAT(x)DOG(y)AFRAID(x,y)CAT(x5)AFRAID(x2,y2)MEOWS(x)FRIENDLY(y)WAGS-TAIL(y)DOG(x1)FRIENDLY(x1)BARKS(y)DOG(FIDO)MEOWS(MYRTLE)BARKS(FIDO)WAGS-TAIL(FIDO)DOG(FIDO)R1R2R5x5/xMYRTLE/xFIDO/yFIDO/yx2/x，y2/yFIDO/yFIDO/yy/x126规章演绎系统(2)规章逆向演绎系统与或图的逆向推理规章变换正向演绎系统能够处理任意形式的if表达式，但被限制在then表达式为由文字析取组成的一些表达式。逆向演绎系统能够处理任意形式的then表达式，但被限制在if表达式为文字合取组成的一些表达式。[CAT(MYRTLE)∧DOG(FIDO)∧AFRAID(MYRTLE,FIDO)]27

谓词演绎的归结方法谓词、函数、量词谓词：表示个体对象之间的关系、属性或状态。其表示形式如下：

P(x1,x2,x3,...xn)

其中：P是谓词符号，表示x1,x2,x3,...xn个体对象之间的属性、状态或关系。x1,x2,x3,...xn是谓词的参量〔或称项〕，一般表示个体，它可以是个体常量、个体变量或是个体函数。个体变元的变化范围称为个体域〔或论域〕例：

P(x):表示x是素数

FRIEND(a,b)：表示a和b是朋友28谓词演绎的归结方法谓词、函数、量词个体函数：表示项之间的关系

有了个体函数之后，谓词的表达力量更强。假设个体函数father(b)表示“个体b的父亲”，则谓词FRIEND(a,father(b))表示“a和b的父亲是朋友”，明显表达力量更强了。例：

E(x,y):表示x和y相等关系

个体函数square(x)：表示个体x的平方

则谓词E(square(a),b)表示什么？29谓词演绎的归结方法谓词、函数、量词量词

全称量词：“全部”,“一切”,“任一”,“全体”,“但凡”等词称为全称量词，记为

存在量词：“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词，记为例：谓词M(x):表示x是人，谓词N(x):表示x知名字，则x(M(x)→N(x))表示“但凡人都知名字”。

谓词G(x):表示x是整数，E(x)：表示x是偶数，则x〔G(x)∧E(x))表示“存在不是偶数的整数”

学问“不存在最大的整数”的表示：谓词D(x,y)表示x大于y。则表示如下：x(G(x)∧y(G(y)→D(x,y)))30谓词演绎的归结方法命题规律中的归结推理方法假设命题规律描述的命题A1,A2,...An和B,要证明在A1∧A2∧...∧An成立的条件下有B成立，或说A1∧A2∧...∧An→B。很明显A1∧A2∧...∧An→B等价于证明A1∧A2∧...∧An∧B是冲突(永假)式。归结推理的方法就是从A1∧A2∧...∧An∧B动身使用归结推理规章来查找冲突，从而证明A1∧A2∧...∧An→B的成立。这种方法称为反演推理方法。31谓词演绎的归结方法命题规律的归结推理过程利用规律蕴含式和规律等价式将命题公式化成合取范式(子句的合取)子句集：将假设干个子句的合取式中的合取词∧换成逗号，形成的集合称为子句集。从子句集S动身，仅只对S的子句间使用归结推理规章〔即求归结式〕，并将所得归结式仍放入S中，进而再对新子句集使用归结推理规章，重复这些步骤直到得到空子句□〔说明有冲突〕。也就是说S是不行满足的，从而与子句集S对应的定理是成立的。32谓词演绎的归结方法谓词公式的子句形合取范式和析取范式

合取范式：假设谓词公式A有如下形式B1∧B2∧...∧Bn,其中Bi(i=1,2,...n)形如L1∨L2∨...∨Ln，并且L1,L2,...Ln都是文字。

析取范式：假设谓词公式A有如下形式B1∨B2∨...∨Bn,其中Bi(i=1,2,...n)形如L1∧L2∧...∧Ln，并且L1,L2,...Ln都是文字。

前束范式：将全部的量词都放在谓词公式的前面。前束范式可分成前束合取范式和前束析取范式。33谓词演绎的归结方法化成前束合取范式的步骤Step1：消去∧，∨，以外的连接词

AB.............A∨B

AB............(A∨B)∧(B∨A)step2：将连接词内移，移到原子公式之前

(A)A

(A∧B)

A∨B

(A∨B)

A∧B

xA(x)

xA(x)

xA(x)

xA(x)34谓词演绎的归结方法化成前束合取范式的步骤Step3：将量词尽可能向左推，推到前缀所在的位置，用以下公式：

xA(x)∨B............x〔A(x)∨B〕，其中B中不含约束变元

B∨xA(x)............x〔B∨A(x)〕，其中B中不含约束变元

xA(x)∨B............x〔A(x)∨B〕，其中B中不含约束变元

B∨xA(x)............x〔B∨A(x)〕，其中B中不含约束变元

同样对上面式子中的∨改为∧可得到另一组关于的∧的替换式。35谓词演绎的归结方法化成前束合取范式的步骤step4：用下式进展替换：

xA(x)∧xB(x)..................x〔A(x)∧B(x)〕

xA(x)∨xB(x)..................xy〔A(x)∨B(y)〕,承受更名规章

xA(x)∨xB(x)..................x〔A(x)∨B(x)〕

xA(x)∧xB(x)..................xy〔A(x)∧B(y)〕,承受更名规章Step5：使用∧，∨的安排律化成合取范式。36谓词演绎的归结方法将谓词公式化成子句集的步骤按上述步骤化成前束合取范式；化成Skolem标准型，消去存在量词；消取存在量词时，还要进展变元替换。变元替换分两种状况：

⑴假设该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数称为Skolem函数；

⑵假设该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中相应约束变元，这样的常量符号称为Skolem常量。37谓词演绎的归结方法将谓词公式化成子句集的步骤消去全部全称量词

消去合取词∧，用逗号代替，以子句为元素组成一个集合S，即是谓词公式的子句集。38谓词演绎的归结方法引入掌握策略从谓词规律的归结方法中我们可以看出，当使用归结法时，假设从子句集S动身做全部可能的归结，并将归结式参加S中，再做其次层这样的归结，…直到产生空子句。这种盲目的归结，会产生组合爆炸问题。这种无掌握的归结导致大量的不必要的归结式的产生。如何给出掌握策略，以使系统仅选择合式的子句对其做归结来避开多余不必要的归结式的消失，或者说少做些归结但仍旧导出空子句来，这已经成为一个重要的问题。39谓词演绎的归结方法引入掌握策略归纳起来，归结过程策略掌握的要点如下：要解决的问题：归结方法避开学问爆炸。掌握策略的目的：归结点尽量少。掌握策略的原则：删除不必要的子句，或对参与归结的子句做限制。给出掌握策略，以使仅选择合式的子句对其做归结。避开多余的、不必要的归结式消失。40谓词演绎的归结方法引入掌握策略置换与合一(含有变量的归结式)在谓词规律中，有些推理规章可应用于肯定的合式公式或合式公式集，以产生新的合式公式。一个重要的推理规章是假言推理，这就是由合式公式W1和W1=>W2产生合式公式W2的运算。另一个推理规章叫做全称化推理，它是由合式公式(x)W(x)产生合式公式W(A)，其中A为任意常量符号。41谓词演绎的归结方法引入掌握策略置换与合一(含有变量的归结式)在谓词规律中，有些推理规章可应用于肯定的合式公式或合式公式集，以产生新的合式公式。一个重要的推理规章是假言推理，这就是由合式公式W1和W1=>W2产生合式公式W2的运算。另一个推理规章叫做全称化推理，它是由合式公式(x)W(x)产生合式公式W(A)，其中A为任意常量符号。综合推理：它是由合式公式(x)W1(x)=>W2(x)，W1(A)产生合式公式W2(A)，其中A为任意常量符号。42谓词演绎的归结方法引入掌握策略置换与合一一个表达式的项可以是常量、变量和函数。合一就是查找项对变量的置换而使表达式全都。置换可用有序对的集合s={t1/v1,t2/v2,…,tn/vn}表示，其中ti/vi表示每个变量vi用ti替换。ti可以是常量或变量或函数。但是f(vi)/vi是不允许的，即在替换中不允许在项中消失被替换的变量。置换是可以结合的，换句话说，假设s1和s2是合式公式E的置换，那么(E)s1s2=((E)s1)s243谓词演绎的归结方法引入掌握策略置换与合一把置换s作用于集合{Ei}中的每个公式得到的例的集合用{Ei}s表示。假设存在一个置换s，使得(E1)s=(E2)s=…=(En)s，那么称公式集合{Ei}为可合一的，置换s称为{Ei}的合一者。下面是递归合一算法UNIFY(E1,E2)；其中，E1,E2是待合一的公式：1、如果E1或E2是原子公式，无妨设是E1则执行22、如果E1和E2是相同的，returnNIL3、如果E1是一个变量则执行4否则到64、如果E1出现在E2中则returnFAIL5、return{E2/E1}6、F1E1的第一个元素，T1E1的其余元素；F2E2的第一个元素，T2E2的其余元素；7、Z1UNIFY(F1,F2)8、如果Z1=FAIL则returnFAIL9、G1Z1作用于T1的结果；G2Z1作用于T2的结果；10、Z2UNIFY(G1,G2)11、如果Z2=FAIL则returnFAIL；否则returnZ1与Z2的合成。44谓词演绎的归结方法在谓词规律中，子句含有变量。这时，查找一个置换，作用于给定的两个子句，使它们包括互补文字，即存在文字1和¬1，然后进展归结。设C1和C2是两个没有一样变量的子句，并分别表示成两个文字集合{Li}和{Mi}，li是{Li}的一个文字，¬mi是{Mi}的一个子集。假设存在s是文字li和mi的最小合一置换，则C12={{Li}-{li}}{{Mi}-{¬mi}}s，为子句C1和C2的归结。更一般定义为：设C1和C2是两个没有一样变量的子句，并分别表示成两个文字集合{Li}和{Mi}，{li}是{Li}的一个子集，{mi}是的一个子集{Mi}。假设s是集合{li}和{¬mi}的并集的最小合一置换，则称C12={{Li}-{li}}{{Mi}-{mi}}s为C1和C2的归结。45谓词演绎的归结方法等式谓词在归结的过程中，通常谓词名的语义并不能真正猎取，因此，有时无法得到正确的结论。例如：假设有Equals(A,B)，但是，无法归结：¬P(A,B)和P(B,A)。因此，需要引入等式谓词：自反性：(x)Equals(x,x)对称性：(x,y)[Equals(x,y)Equals(y,x)]传递性：(x,y,z)[Equals(x,y)Equals(y,z)Equals(x,z)]46谓词演绎的归结方法等式谓词在归结的过程中，通常谓词名的语义并不能真正猎取，因此，有时无法得到正确的结论。即使有等式谓词有了这些公理，但还是无法得到，例：{P(A)，Equals(A,B)}P(B)。于是，我们给出等价替换规章：假设有两个子句：1，2。1={()1’}，2={Equals(,)2’}其中，，，是项。1’和2’子句。()是包含的文字。假设有一置换使得，能够合一，那么有1’和2’的调解式：={[()]1’2’}该调解式实际上，是将中用替换，并且与1’和2’做析取。47归结反对搜寻策略排序策略定义n层归结项：1〕把原子的子句称为0层归结项；2〕i+1层的归结项是一个i层归结项和一个j层归结项归结的结果。广度优先：依据归结项的层数每次产生该层的全部归结项，逐层生成，直到或者产生了空子句，或者不能再产生新的层次。深度优先：首先产生一个第1层的归结项，然后，用某些第1层的归结项或0层归结项产生第2层的归结项，依次类推。排序归结的一个通用策略是单元优先策略：这种归结至少有一个子句有一个单一的文字构成。这样的子句称为单元子句。48归结反对搜寻策略准确策略支持集的概念：子句2是另一个子句1的后裔，当且仅当：(a)2是1和另一些子句的一个归结项；或(b)2是1的后裔与另一些子句的一个归结项。2是1的后裔，那么1是2的祖先。支持集定义为由一些子句组成，这些子句或来源于待证定理的否认，或者是这些子句的后裔。支持集策略：只允许这样一些归结：在其中正在被归结的子句中的一个在支持集中。支持集策略是反对完备的。即，假设只对一个不行满足的子句集合运用支持集归