1、谓词逻辑基础谓词逻辑基础一阶逻辑一阶逻辑l基本概念基本概念l个体词：表示主语的词个体词：表示主语的词l谓词：刻画个体性质或个体之间关系的词谓词：刻画个体性质或个体之间关系的词l量词：表示数量的词量词：表示数量的词l小王是个工程师。小王是个工程师。l8是个自然数。是个自然数。l我去买花。我去买花。l小丽和小华是朋友。小丽和小华是朋友。其中，其中，“小王小王”、“工程师工程师”、“我我”、“花花”、“8”、“小丽小丽”、“小华小华”都是个体词，而都是个体词，而“是个工程师是个工程师”、“是个自然数是个自然数”、“去买去买”、“是朋友是朋友”都是谓词。显然前两个谓词表示的是事物都是谓词。显然前两个谓
2、词表示的是事物的性质，第三个谓词的性质，第三个谓词“去买去买”表示的一个动作也表示了主、宾两表示的一个动作也表示了主、宾两个个体词的关系，最后一个谓词个个体词的关系，最后一个谓词“是朋友是朋友”表示两个个体词之间表示两个个体词之间的关系。的关系。谓词逻辑基础谓词逻辑基础谓词逻辑基础谓词逻辑基础l例如：（例如：（1）所有的人都是要死的。）所有的人都是要死的。l （2）有的人活到一百岁以上。有的人活到一百岁以上。在个体域在个体域D为人类集合时，可符号化为：为人类集合时，可符号化为：（1）xPxP(x x)，其中，其中P P(x x)表示表示x x是要死的。是要死的。（2）x Qx Q(x x),)
3、,其中其中Q Q(x x)表示表示x x活到一百岁以上。活到一百岁以上。在个体域在个体域D是全总个体域时，是全总个体域时，引入特殊谓词引入特殊谓词R R(x x)表示表示x x是人，可符号化为：是人，可符号化为：（1 1）x x（R R(x x)P P(x x)）,其中，其中，R R(x x)表示表示x x是人；是人；P P(x x)表示表示x x是要死的。是要死的。（2 2）x x（R R(x x)Q Q(x x)），），其中，其中，R R(x x)表示表示x x是人；是人；Q Q(x x)表示表示x x活到一百岁以上。活到一百岁以上。一阶逻辑一阶逻辑l公式及其解释公式及其解释l个体常量：个
4、体常量：a,b,cl个体变量：个体变量：x,y,zl谓词符号：谓词符号：P,Q,Rl量词符号：量词符号：,谓词逻辑基础谓词逻辑基础量词否定等值式：量词否定等值式：l(x x ）P P（x x）（y y ）P P（y y）l(x x ）P P（x x）（y y ）P P（y y）量词分配等值式：量词分配等值式：l(x x ）(P P（x x）Q Q（x x）)()(x x ）P P（x x）(x x ）Q Q（x x）l(x x ）(P P（x x）Q Q（x x）)()(x x ）P P（x x）(x x ）Q Q（x x）消去量词等值式：消去量词等值式：设个体域为有穷集合（设个体域为有穷集合
5、（a a1 1,a,a2 2,a an n）l(x x ）P P（x x）P P（a a1 1 ）P P（a a2 2 ）P P（a an n ）l(x x ）P P（x x）P P（a a1 1 ）P P（a a2 2 ）P P（a an n ）谓词逻辑基础谓词逻辑基础量词辖域收缩与扩张等值式：量词辖域收缩与扩张等值式：l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Ql(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(Q Q P P（x x
6、）)Q Q (x x ）P P（x x）l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Ql(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(Q Q P P（x x）)Q Q (x x ）P P（x x）谓词逻辑基础谓词逻辑基础谓词逻辑基础谓词逻辑基础SKOLEMSKOLEM标准形标准形l前束范式前束范式定义定义：说公式：说公式A A是一个前束范式，如果是一个前束范式，如果A A中中的一切量词都位于该公式的最左边（不含否的一切量词都位于该公式的
7、最左边（不含否定词），且这些量词的辖域都延伸到公式的定词），且这些量词的辖域都延伸到公式的末端。末端。谓词逻辑归结原理谓词逻辑归结原理即：即：把所有的量词都提到前面去，然后消把所有的量词都提到前面去，然后消掉所有量词掉所有量词(Q(Q1 1x x1 1)(Q)(Q2 2x x2 2)(Q(Qn nx xn n)M(x)M(x1 1,x,x2 2,x,xn n)约束变项换名规则：约束变项换名规则：l(Qx(Qx ）MM（x x）（QyQy ）MM（y y）l(Qx(Qx ）MM（x,zx,z）（QyQy ）MM（y,zy,z）谓词逻辑归结原理谓词逻辑归结原理l l l l l l l l l l
8、 l l l l l l l l l l l l l l l ll量词消去原则：量词消去原则：消去存在量词消去存在量词“”，略去全程量词，略去全程量词“”。注意：注意：左边有全程量词的存在量词，消去左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数；如没时该变量改写成为全程量词的函数；如没有，改写成为常量。有，改写成为常量。谓词逻辑归结原理谓词逻辑归结原理l l l l l l l l l l l l l l l l l l l l l l l l l llSkolemSkolem定理定理：谓词逻辑的任意公式都可以化为与之等价谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范
9、式不唯一。的前束范式，但其前束范式不唯一。lSKOLEMSKOLEM标准形定义：标准形定义：消去量词后的谓词公式。消去量词后的谓词公式。注意注意：谓词公式：谓词公式G G的的SKOLEMSKOLEM标准形同标准形同G G并并不等值不等值。谓词逻辑归结原理谓词逻辑归结原理例：例：将下式化为将下式化为Skolem标准形：标准形：(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)l解：第一步，消去解：第一步，消去号，得：号，得：(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)l第二步，深入到量词内部，得：第二步，深入到量词内部，得：(x)(y)P(a,x,y)(x)x)(y)Q
10、(y,b)R(x)l第三步，变元易名，得第三步，变元易名，得(x)(y)P(a,x,y)(u)(v)(Q(v,b)R(u)l第四步，存在量词左移，直至所有的量词移到前面，第四步，存在量词左移，直至所有的量词移到前面，(x)(y)(u)(v)(P(a,x,y)(Q(v,b)R(u)由此得到前述范式由此得到前述范式l第五步，消去第五步，消去“”（存在量词），略去（存在量词），略去“”全称量全称量词词l消去消去(y)，因为它左边只有，因为它左边只有(x)，所以使用，所以使用x的函数的函数f(x)代替之，这样得到：代替之，这样得到：(x)(u)(v)(P(a,x,f(x)Q(v,b)R(u)l消去消去
11、(u)，同理使用，同理使用g(x)代替之，这样得到：代替之，这样得到：(x)(v)(P(a,x,f(x)Q(v,b)R(g(x)l则，略去全称变量，原式的则，略去全称变量，原式的Skolem标准形为：标准形为：P(a,x,f(x)Q(v,b)R(g(x)l子句与子句集子句与子句集l文字：不含任何连接词的谓词公式。文字：不含任何连接词的谓词公式。l子句：一些文字的析取（谓词的和）。子句：一些文字的析取（谓词的和）。l子句集子句集S S的求取：的求取：G G SKOLEM SKOLEM标准形标准形 消去存在变量消去存在变量 以以“，”取代取代“”，并表示为集合形式，并表示为集合形式 。谓词逻辑归结
12、原理谓词逻辑归结原理l G是不可满足的是不可满足的 S是不可满足的是不可满足的lG与与S不等价，但在不可满足得意义下是一致的。不等价，但在不可满足得意义下是一致的。l定理：定理：若若G是给定的公式，而是给定的公式，而S是相应的子句集，则是相应的子句集，则G是是不可满足的不可满足的 S是不可满足的。是不可满足的。注意注意：G真不一定真不一定S真，而真，而S真必有真必有G真。真。即：即：S=G谓词逻辑归结原理谓词逻辑归结原理lG=GG=G1 1 G G2 2 G G3 3 G Gn n 的子句形的子句形lG G的字句集可以分解成几个单独处理。的字句集可以分解成几个单独处理。l有有 S SG G=S
13、=S1 1 U SU S2 2 U S U S3 3 U U U SU Sn n则则S SG G 与与 S S1 1 U SU S2 2 U S U S3 3 U U U SU Sn n在不可满足得意义在不可满足得意义上是一致的。上是一致的。即即S SG G 不可满足不可满足 S S1 1 U SU S2 2 U S U S3 3 U U U SU Sn n不可满足不可满足3.3 谓词逻辑归结原理谓词逻辑归结原理例：对所有的例：对所有的x,y,z来说，如果来说，如果y是是x的父亲，的父亲，z又是又是y的的父亲，则父亲，则z是是x的祖父。又知每个人都有父亲，试问对的祖父。又知每个人都有父亲，试问
14、对某个人来说谁是它的祖父？某个人来说谁是它的祖父？求：用一阶逻辑表示这个问题，并建立子句集。求：用一阶逻辑表示这个问题，并建立子句集。解：这里我们首先引入谓词：解：这里我们首先引入谓词：lP(x,y)表示表示x是是y的父亲的父亲lQ(x,y)表示表示x是是y的祖父的祖父lANS(x)表示问题的解答表示问题的解答谓词逻辑归结原理谓词逻辑归结原理对于第一个条件，对于第一个条件，“如果如果x是是y 的父亲，的父亲，y又是又是z 的父亲，则的父亲，则x是是z 的祖父的祖父”，一阶逻辑表达式如下：，一阶逻辑表达式如下：A1：(x)(y)(z)(P(x,y)P(y,z)Q(x,z)S A1：P(x,y)P
15、(y,z)Q(x,z)对于第二个条件：对于第二个条件：“每个人都有父亲每个人都有父亲”，一阶逻辑表达式：，一阶逻辑表达式：A2：(y)(x)P(x,y)S A2：P(f(y),y)对于结论：某个人是它的祖父对于结论：某个人是它的祖父B：(x)(y)Q(x,y)否定后得到子句：否定后得到子句：（(x)(y)Q(x,y)）ANS(x)SB：Q(x,y)ANS(x)则得到的相应的子句集为：则得到的相应的子句集为：S A1，S A2，SB 谓词逻辑归结原理谓词逻辑归结原理l归结原理正确性的根本在于，找到矛盾归结原理正确性的根本在于，找到矛盾可以肯定不真。可以肯定不真。l方法：方法：l和命题逻辑一样。和
16、命题逻辑一样。l但由于有函数，所以要考虑但由于有函数，所以要考虑合一合一和和置换置换。谓词逻辑归结原理谓词逻辑归结原理l置换：可以简单的理解为是在一个谓词公式中用置换项去置换变置换：可以简单的理解为是在一个谓词公式中用置换项去置换变量。量。l定义：定义：置换是形如置换是形如t1/x1,t2/x2,tn/xn的有限集合。其中，的有限集合。其中，x1,x2,xn是互不相同的变量，是互不相同的变量，t1,t2,tn是不同于是不同于xi的项（常量、变量、函的项（常量、变量、函数）；数）；ti/xi表示用表示用ti置换置换xi，并且要求，并且要求ti与与xi不能相同，而且不能相同，而且xi不能不能循环地
17、出现在另一个循环地出现在另一个ti中。中。例如例如a/x，c/y，f(b)/z是一个置换。是一个置换。g(y)/x，f(x)/y不是一个置换，不是一个置换，谓词逻辑归结原理谓词逻辑归结原理置换置换置换的合成置换的合成l设设 t1/x1,t2/x2,tn/xn，u1/y1,u2/y2,un/yn，是两个置换。，是两个置换。则则 与与 的合成也是一个置换，记作的合成也是一个置换，记作 。它是从集合。它是从集合t1/x1,t2/x2,tn/xn,u1/y1,u2/y2,un/yn 中删去以下两种元素：中删去以下两种元素：li.当当ti=xi时，删去时，删去ti/xi(i=1,2,n);lIi.当当y
18、i x1,x2,xn时，删去时，删去uj/yj(j=1,2,m)最后剩下的元素所构成的集合。最后剩下的元素所构成的集合。合成即是对合成即是对ti先做先做 置换然后再做置换然后再做 置换，置换置换，置换xi谓词逻辑归结原理谓词逻辑归结原理l例：例：设：设：f(y)/x,z/y，a/x,b/y,y/z，求，求 与与 的合成。的合成。解：先求出集合解：先求出集合f(b/y)/x,(y/z)/y,a/x,b/y,y/zf(b)/x,y/y,a/x,b/y,y/z其中，其中，f(b)/x中的中的f(b)是置换是置换 作用于作用于f(y)的结果；的结果；y/y中的中的y是置换是置换 作用于作用于z的结果。
19、在该集合中，的结果。在该集合中，y/y满足定义中的条满足定义中的条件件i，需要删除；，需要删除；a/x，b/y满足定义中的条件满足定义中的条件ii，也需要删除。，也需要删除。最后得最后得 f(b)/x，y/z谓词逻辑归结原理谓词逻辑归结原理合一合一l合一可以简单地理解为合一可以简单地理解为“寻找相对变量的置换，使两个谓词寻找相对变量的置换，使两个谓词公式一致公式一致”。l定义：设有公式集定义：设有公式集FF1，F2，Fn，若存在一个置换，若存在一个置换，可使可使F1 F2=Fn，则称，则称 是是F的一个合一。同时称的一个合一。同时称F1，F2，.，Fn是可合一的。是可合一的。l 例：例：设有公
20、式集设有公式集FP(x,y,f(y),P(a,g(x),z)，则，则 a/x,g(a)/y,f(g(a)/z是它的一个合一。是它的一个合一。注意：一般说来，一个公式集的合一不是唯一的。注意：一般说来，一个公式集的合一不是唯一的。谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理谓词逻辑归结原理归结原理归结原理l归结的注意事项：归结的注意事项：1.1.谓词的一致性谓词的一致性，P()P()与与Q()Q()，不可以不可以2.2.常量的一致性，常量的一致性，P(a,P(a,)与与P(b,P(b,.).)，不可以不可以 变量，变量，P(a,
21、P(a,.).)与与P(x,P(x,)，可以可以3.3.变量与函数，变量与函数，P(a,x,P(a,x,.).)与与P(x,f(x),P(x,f(x),)，不，不可以；可以；3.3.是不能同时消去两个互补对，是不能同时消去两个互补对，PQPQ与与PPQ Q的空，的空，不可以不可以4.4.先进行内部简化（置换、合并）先进行内部简化（置换、合并）谓词逻辑归结原理谓词逻辑归结原理l归结的过程归结的过程写出谓词关系公式写出谓词关系公式 用反演法写出谓词表达式用反演法写出谓词表达式 SKOLEMSKOLEM标准形标准形 子句集子句集S S 对对S S中可归结的子句做归结中可归结的子句做归结 归结式仍放入
22、归结式仍放入S S中，反复归结过程中，反复归结过程 得到空子句得到空子句 得证得证谓词逻辑归结原理谓词逻辑归结原理例题例题“快乐学生快乐学生”问题问题l假设任何通过计算机考试并获奖的人都是快乐的，任假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。张是快乐的。l 解：先将问题用谓词表示如下：解：先将问题用谓词表示如下：lR1:“任何通过计算机考试并获奖的人都是快乐的任何通过计算机考试并获奖的人都是快乐的”
23、(x)(Pass(x,computer)Win(x,prize)Happy(x)lR2:“任何肯学习或幸运的人都可以通过所有考试任何肯学习或幸运的人都可以通过所有考试”(x)(y)(Study(x)Lucky(x)Pass(x,y)lR3:“张不肯学习但他是幸运的张不肯学习但他是幸运的”Study(zhang)Lucky(zhang)lR4:“任何幸运的人都能获奖任何幸运的人都能获奖”(x)(Luck(x)Win(x,prize)l结论：结论：“张是快乐的张是快乐的”的否定的否定Happy(zhang)例题例题“快乐学生快乐学生”问题问题l由由R1及逻辑转换公式及逻辑转换公式:PWH=（PW）
24、H，可得，可得l (1)Pass(x,computer)Win(x,prize)Happy(x)l由由R2：(2)Study(y)Pass(y,z)l (3)Lucky(u)Pass(u,v)l由由R3：(4)Study(zhang)l (5)Lucky(zhang)l由由R4：(6)Lucky(w)Win(w，prize)l由结论：由结论：(7)Happy(zhang)（结论的否定）（结论的否定）l(8)Pass(w,computer)Happy(w)Luck(w)(1)(6)，w/xl(9)Pass(zhang,computer)Lucky(zhang)(8)(7)，zhang/wl(10
25、)Pass(zhang,computer)(9)(5)l(11)Lucky(zhang)(10)(3)，zhang/u,computer/vl(12)(11)(5)l归结法的实质：归结法的实质：l归结法是仅有一条推理规则的推理方法。归结法是仅有一条推理规则的推理方法。l归结的过程是一个语义树倒塌的过程。归结的过程是一个语义树倒塌的过程。l归结法的问题归结法的问题l子句中有等号或不等号时，完备性不成立。子句中有等号或不等号时，完备性不成立。Herbrand Herbrand定理的不实用性引出了可实用的定理的不实用性引出了可实用的归结法。归结法。谓词逻辑归结原理谓词逻辑归结原理归结过程的控制策略归
26、结过程的控制策略l要解决的问题：要解决的问题：l归结方法的知识爆炸。归结方法的知识爆炸。l控制策略的目的控制策略的目的l归结点尽量少归结点尽量少l控制策略的原则控制策略的原则l给出控制策略，以使仅对选择合适的子句给出控制策略，以使仅对选择合适的子句间方可做归结。避免多余的、不必要的归间方可做归结。避免多余的、不必要的归结式出现。或者说，少做些归结仍能导出结式出现。或者说，少做些归结仍能导出空子句。空子句。谓词逻辑归结原理谓词逻辑归结原理删除策略删除策略=完备完备l名词解释：归类：设有两个子句名词解释：归类：设有两个子句C C和和D D，若有置换，若有置换 使得使得C C D D成立，则称子句成
27、立，则称子句C C把子句把子句D D归类。归类。由于小的可以代表大的，所以小的吃掉大的了。由于小的可以代表大的，所以小的吃掉大的了。l若对若对S S使用归结推理过程中，当归结式使用归结推理过程中，当归结式C Cj j是重言式是重言式（永真式）和（永真式）和C Cj j被被S S中子句和子句集的归结式中子句和子句集的归结式C Ci i(ij)(ij)所归类时，便将所归类时，便将C Cj j删除。这样的推理过程便称做使删除。这样的推理过程便称做使用了删除策略的归结过程。用了删除策略的归结过程。谓词逻辑归结原理谓词逻辑归结原理l主要思想：归结过程在寻找可归结子句时，子主要思想：归结过程在寻找可归结子
28、句时，子句集中的子句越多，需要付出的代价就会越大。句集中的子句越多，需要付出的代价就会越大。如果在归结时能把子句集中无用的子句删除掉，如果在归结时能把子句集中无用的子句删除掉，就会缩小搜索范围，减少比较次数，从而提高就会缩小搜索范围，减少比较次数，从而提高归结效率。删除策略对阻止不必要的归结式的归结效率。删除策略对阻止不必要的归结式的产生来缩短归结过程是有效的。然而要在归结产生来缩短归结过程是有效的。然而要在归结式式C Cj j产生后方能判别它是否可被删除，这部分产生后方能判别它是否可被删除，这部分计算量是要花费的，只是节省了被删除的子句计算量是要花费的，只是节省了被删除的子句又生成的归结式。
29、尽管使用删除策略的归结，又生成的归结式。尽管使用删除策略的归结，少做了归结但不影响产生空子句，就是说删除少做了归结但不影响产生空子句，就是说删除策略的归结推理是完备的。策略的归结推理是完备的。谓词逻辑归结原理谓词逻辑归结原理采用支撑集采用支撑集 完备完备 支撑集：设有不可满足子句集支撑集：设有不可满足子句集S S的子集的子集T T，如，如果果S-TS-T是可满足的，则是可满足的，则T T是支持集。是支持集。采用支撑集策略时，从开始到得到采用支撑集策略时，从开始到得到的整个的整个归结过程中，只选取不同时属于归结过程中，只选取不同时属于S-TS-T的子句，的子句，在其间进行归结。就是说，至少有一个
30、子在其间进行归结。就是说，至少有一个子句来自于支撑集句来自于支撑集T T或由或由T T导出的归结式。导出的归结式。谓词逻辑归结原理谓词逻辑归结原理例如：例如：A A1 1AA2 2AA3 3B B中的中的B B可以作为支撑集使用。可以作为支撑集使用。要求每一次参加归结的亲本子句中，只要应该有一个是要求每一次参加归结的亲本子句中，只要应该有一个是有目标公式的否定（有目标公式的否定（B B）所得到的子句或者它们的后）所得到的子句或者它们的后裔。裔。l支撑集策略的归结是完备的，同样，所有可归结的谓词支撑集策略的归结是完备的，同样，所有可归结的谓词公式都可以用采用支撑集策略达到加快归结速度的目的。公式
31、都可以用采用支撑集策略达到加快归结速度的目的。问题是如何寻找合适的支撑集。一个最容易找到的支撑问题是如何寻找合适的支撑集。一个最容易找到的支撑集是目标子句的非，即集是目标子句的非，即S SB B。谓词逻辑归结原理谓词逻辑归结原理ST可满足支撑集示意图谓词逻辑归结原理谓词逻辑归结原理 语义归结语义归结 完备完备 语义归结策略是将子句语义归结策略是将子句S S按照一定的语义按照一定的语义分成两部分，约定每部分内的子句间不允许分成两部分，约定每部分内的子句间不允许作归结。同时还引入了文字次序，约定归结作归结。同时还引入了文字次序，约定归结时其中的一个子句的被归结文字只能是该子时其中的一个子句的被归结
32、文字只能是该子句中句中“最大最大”的文字。的文字。语义归结策略的归结是完备的，同样，语义归结策略的归结是完备的，同样，所有可归结的谓词公式都可以用采用语义归所有可归结的谓词公式都可以用采用语义归结策略达到加快归结速度的目的。问题是如结策略达到加快归结速度的目的。问题是如何寻找合适的语义分类方法，并根据其含义何寻找合适的语义分类方法，并根据其含义将子句集两个部分中的子句进行排序。将子句集两个部分中的子句进行排序。谓词逻辑归结原理谓词逻辑归结原理线性归结线性归结 完备完备 线性归结策略首先从子句集中选取一个称作顶线性归结策略首先从子句集中选取一个称作顶子句的子句子句的子句C C0 0开始作归结。归
33、结过程中所得到的归开始作归结。归结过程中所得到的归结式结式C Ci i立即同另一子句立即同另一子句B Bi i进行归结得归结式进行归结得归结式C Ci+1i+1。而。而B Bi i属于属于S S或是已出现的归结式或是已出现的归结式C Cj j(ji)(j=完备完备 单元归结策略要求在归结过程中，每次归结都单元归结策略要求在归结过程中，每次归结都有一个子句是单元子句（只含一个文字的子句）有一个子句是单元子句（只含一个文字的子句）或单元因子。显而易见，词中方法可以简单地削或单元因子。显而易见，词中方法可以简单地削去另一个非单子句中的一个因子，使其长度减少，去另一个非单子句中的一个因子，使其长度减少
34、，构成简单化，归结效率较高。构成简单化，归结效率较高。初始子句集中没有单元子句时，单元归结策略初始子句集中没有单元子句时，单元归结策略无效。所以说无效。所以说“反之不成立反之不成立”，即此问题不能采，即此问题不能采用单元归结策略用单元归结策略。输入归结输入归结 =完备完备 与单元归结策略相似，输入归结策略要求在归结与单元归结策略相似，输入归结策略要求在归结过程中，每一次归结的两个子句中必须有一个是过程中，每一次归结的两个子句中必须有一个是S S的的原始子句。这样可以避免归结出的不必要的新子句原始子句。这样可以避免归结出的不必要的新子句加入归结，造成恶性循环。可以减少不必要的归结加入归结，造成恶性循环。可以减少不必要的归结次数。次数。如同单元归结策略，不是所有的可归结谓如同单元归结策略，不是所有的可归结谓词公式的最后结论都是可以从原始子句集词公式的最后结论都是可以从原始子句集中的得到的。简单的例子，归结结束时，中的得到的。简单的例子，归结结束时，即最后一个归结式为空子句的条件是，参即最后一个归结式为空子句的条件是，参加归结的双方必须是两个单元子句。原始加归结的双方必须是两个单元子句。原始子句集中没有单元子句的谓词公式一定不子句集中没有单元子句的谓词公式一定不能采用输入归结策略。能采用输入归结策略。
