《吉林大学研究生人工智能t演示文档》由会员分享，可在线阅读，更多相关《吉林大学研究生人工智能t演示文档（127页珍藏版）》请在金锄头文库上搜索。
1、第六章第六章归结原理归结原理6.1 子句集的子句集的Herbrand域域 一、一、 Herbrand域与域与 Herbrand解释解释l定定义义（Herbrand域域）设设S为为子子句句集集，令令H0是是出出现现于于子子句句集集S的的常常量量符符号号集集。如如果果S中中无无常常量量符符号号出出现现，则则H0由一个常量符号由一个常量符号a组组成。成。 对对于于i1，2，令，令 Hi = Hi-1 所有形如所有形如f(t1，tn)的的项项 其中其中f(t1，tn)是出是出现现在在S中的所有中的所有n元函数符号，元函数符号， tj Hi-1，j1，n 称称Hi为为S的的i级级常量集，常量集，H 称称
2、为为S的的Herbrand域，域， 简简称称S的的H域。域。.l例例SP(f(x)，a，g(y)，b) H0 =a, b H1 =a, b, f(a), f(b), g(a), g(b) H2a, b, f(a), f(b), g(a), g(b), f(f(a), f(f(b), f(g(a), f(g(b), g(f(a), g(f(b), g(g(a), g(g(b).练习练习:求S的Herbrand域lSP(x) Q(y)，R(z) lSQ(a) P(f(x)， Q(b) P(g(x,y) .原子集原子集基例基例l基：把对象中的变量用常量代替后得到的无变量符号出现的对象。基：把对象中的
3、变量用常量代替后得到的无变量符号出现的对象。基项、基项集、基原子、基原子集合、基文字、基子句、基项、基项集、基原子、基原子集合、基文字、基子句、基子句集基子句集l定定义义 (原子集、原子集、Herbrand底底) 设设S是子句集，形是子句集，形如如P(t1,tn)的基原子集合，称的基原子集合，称为为S的的Herbrand底底或或S的原子集的原子集 其中其中P(x1，xn)是出是出现现于于S的所有的所有n元元谓词谓词符号，符号，t1，tn是是S的的H域中的元素域中的元素l定定义义（基例）（基例）设设S是子句集，是子句集，C是是S中的一个子中的一个子句用句用S的的H域中元素代替域中元素代替C中所有
4、中所有变变量所得到的量所得到的基子句称基子句称为为子句子句C的基例。的基例。.练习练习l已知已知SP(f(x)，a，g(y)，b)，求，求S的原子集，的原子集， 给给出出P(f(x)，a，g(y)，b)的一个基例。的一个基例。l已知已知SP(x) Q(y)，R(z) ，求，求S的原子集，的原子集， 分分别给别给出出P(x) Q(y)， R(z)的所有基例。的所有基例。l已知已知S Q(a) P(f(x)，Q(b) P(g(x,y)， 求求S的原子集，的原子集， 分分别给别给出出Q(a) P(f(x) ， Q(b) P(g(x,y)的一个基例。的一个基例。l设设SP(x), Q(f(y) R(y
5、) ，求，求S的的H域，域， S的原子集，的原子集， P(x)的基例的基例, Q(f(y) R(y) 的基例。的基例。.H解释解释定定义义（子子句句集集的的H解解释释） 设设S是是子子句句集集，H是是S的的H域域，I*是是S在在H上上的一个解的一个解释释称称I*为为S的一个的一个H解解释释，如果，如果I*满满足如下条件：足如下条件： 1） I*映射映射S中的所有常量符号到自身。中的所有常量符号到自身。 2）若）若f是是S中中n元函数符号，元函数符号，h1，hn是是H中元素，中元素，则则I*指定映射：指定映射： (h1，hn) f (h1，hn) 设设A=A1，A2，An， 是是S的的原原子子集
6、集。于于是是S的的一一个个H解解释释I可方便地表示可方便地表示为为如下一个集合：如下一个集合： I* m1，m2，mn，其中其中, mi =.H解释的例子例例S=P(x)Q(x),R(f(y)S的H域=a,f(a),f(f(a),S的原子集：A=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),S的H解释：I1*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),I2*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),.练习练习S=P(x)Q(x),P(a),Q(b)，求S的所有H解释。.二、二、Herbrand解释与普通解释
7、的关系解释与普通解释的关系l子句集子句集S的的H解释是解释是S的普通解释。的普通解释。lS的普通解释不一定是的普通解释不一定是S的的H解释：普通解释不解释：普通解释不是必须定义在是必须定义在H域上，即使定义在域上，即使定义在H域上，也域上，也不一定是一个不一定是一个H解释。解释。l任取普通解释任取普通解释I，依照，依照I，可以按如下方法构造，可以按如下方法构造S的一个的一个H解释解释I*，使得若，使得若S在在I下为真则下为真则S在在I*下也为真。下也为真。.例.SP(x), Q(y,f(y,a)令令S的一个解的一个解释释I如下：如下： D1，2 a f(1, 1) f(1, 2) f(2, 1
8、) f(2, 2) 2 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2) T F F T F T对应对应于于I的的H解解释释I*： I*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), .例例S=P(x), Q(y, f(y, z)令令S的一个解的一个解释释I如下如下: D=1, 2 f(1, 1) f(1, 2) f(2, 1) f(2, 2) 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2)
9、T F F T F T指定指定 a对应对应1得得H解解释释：I1*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), 指定指定 a对应对应2得得H解解释释： I2*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), .对应对应于于I的的H解解释释I*定定义义（对对应应于于I的的H解解释释I*）设I是子句集S在区域D上的解释。H是S的H域。l是如下递归定义的H到D的映射：1）若S中有常量符号,H0是出现
10、在S中所有常量符号的集合。对任意aH0，规定(a)=I(a)若S中无常量符号,H0=a。规定(a)=d,dD。2）对任意(h1,hn)Hin,及S中任意n元函数符号f(x1,xn),规定(f(h1，hn)=I(f(h1，hn)。.对应对应于于I的的H解解释释I*l对应对应于于I的的H解解释释I*是如下的一个是如下的一个H解解释释： 任取任取S中中n元元谓词谓词符号符号P(x1,xn)， 任取任取(h1,hn) Hn，规规定定 TI*(P(h1，hn)=TI(P(h1 ，hn ).引理引理如果某区域如果某区域D上的解释上的解释I满足子句集满足子句集S，则对应于则对应于I的任意一个的任意一个H解释
11、解释I*也满足也满足S。证证明明：令令S= x1 xn (C1 Cm)，其其中中Ci为为子子句句（i=1, ,m）。由由已已知知TI(S)=T，即即对对任任意意（x1，xn） Dn，都有，都有TI(Ci（x1，xn）)=T, i=1, ,m.因因为对为对S中任意中任意r元元谓词谓词符号符号P（x1，xr）和任意（）和任意（h1，hr） Hr，都有，都有TI*( P（h1，hr）)=TI(P（h1 ，hr ）)其中（其中（h1 ，hr ） Dr。所以，所以，对对任意（任意（h1，hn） Hn，都有，都有TI*( Ci（h1，hn）)=TI(Ci（h1 ，hn ）) 其中（其中（h1 ，hn ）
12、Dn。 i=1, ,m。 故故对对任意（任意（h1，hn） Hn ，都有，都有 TI*(Ci（h1，hn）)=T, 故故TI*(S)=T，即，即I*满满足足S。.只考虑子句集的只考虑子句集的H解释是否够用？解释是否够用？定理定理子句集子句集S恒假当且仅当恒假当且仅当S被其所有被其所有H解释弄假。解释弄假。证明证明:必要性显然。必要性显然。充分性。假设充分性。假设S被其所有被其所有H解释弄假，而解释弄假，而S又是可满足的。又是可满足的。设解释设解释I满足满足S，于是由引理知，对应于，于是由引理知，对应于I的的H解释解释I*也满足也满足S，矛盾故，矛盾故S是不可满足的是不可满足的从现在起，如不特别
13、指出，提到的解释都是指从现在起，如不特别指出，提到的解释都是指H解释解释.结论结论l）子句）子句C的基例的基例C被解释被解释I满足，当且仅当满足，当且仅当C中的一个基文字中的一个基文字L出现在出现在I中中C= P(x) Q(f(y),a) R(z)C= P(a) Q(f(a),a) R(f(a).2）子句）子句C被解释被解释I满足，当且仅当满足，当且仅当C的每一个基例都被的每一个基例都被I满足满足3）子句）子句C被解释被解释I弄假，当且仅当弄假，当且仅当至少有一个至少有一个C的基例的基例C被被I弄假。弄假。.例例.C=P(x) Q(f(x)I1=P(a),Q(a),P(f(a),Q(f(a),
14、P(f(f(a),Q(f(f(a),I2=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a),I3=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a), 显显然，然，I1，I2满满足足C，I3弄假弄假C。.4）子句集）子句集S不可满足，当且仅当不可满足，当且仅当对每个解释对每个解释I，至少有一个，至少有一个S中某个子句中某个子句C的的基例基例C被被I弄假。弄假。.6.2Herbrand定理定理Herbrand定理是符号逻辑中一个很重要的定理Herbrand定理就是使用语义树的方法，把需要考虑无穷个H解释的问题，变成只考虑有限个解释
15、的问题.一、语义树l定义定义(互补对互补对)设设A是原子，两个文字是原子，两个文字A和和A都是另一个的补，集合都是另一个的补，集合A，A称为一个互称为一个互补对补对l定义定义(Tautology,重言式重言式)含有互补对的子句含有互补对的子句.l定义定义（语义树语义树） 设设S是子句集，是子句集，A是是S的原子集关于的原子集关于S的的语义树语义树是一棵向下生是一棵向下生长长的的树树T在在树树的每一的每一节节上都以如下上都以如下方式附着方式附着A中有限个原子或原子的否定：中有限个原子或原子的否定： 1）对对于于树树中每一个中每一个节节点点N，只能向下引出有限的直接的，只能向下引出有限的直接的节节
16、 L1，Ln 设设Qi是附着在是附着在Li上所有文字的合取，上所有文字的合取，i=1, ,n， 则则Q1 Qn是一个恒真的命是一个恒真的命题题公式公式2）对树对树中每一个中每一个节节点点 N，设设 I（N）是）是树树T由根向下到由根向下到节节点点 N 的所有的所有节节上附着文字的并集，上附着文字的并集， 则则I（N）不含任何互）不含任何互补对补对语义树.完全语义树定定义义（完全（完全语义树语义树） 设设A=A1,An,是子句集是子句集S的原子集的原子集 S的一个的一个语义树语义树是完全的，当且是完全的，当且仅仅当当 对对于于语义树语义树中每一个尖端中每一个尖端节节点点N（即从（即从N不再不再
17、生出生出节节的那种的那种节节点），都有点），都有 Ai或或Ai有且有且仅仅有一个属于有一个属于I(N),i=1,k,.例例.设A=P，Q，R是子句集S的原子集，完全完全语义树语义树(正正规规完全完全语义树语义树 )RRRRRRRRQQQQPP.Q,RRRQQRRRRRRPPRQP,QQP.例.设设S=P(x),Q(f(x)S的原子集为A=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a),P(a)P(a)Q(a)Q(a)P(f(a)Q(a)Q(a)P(f(a)Q(f(a)Q(f(a).语义树与解释语义树与解释lS的完全语义树的每一个分枝都对应着的完全语义树的每一
18、个分枝都对应着S的一个解释；的一个解释；定义（部分解释）定义（部分解释）对于子句集对于子句集S的语义树中的每一个节点的语义树中的每一个节点N,I(N)是是S的某个解释的子集，称的某个解释的子集，称I(N)为为S的部分解释。的部分解释。lS的任意解释都对应着的任意解释都对应着S的完全语义树中的一条分枝？的完全语义树中的一条分枝？综合：综合：子句集子句集S的一棵完全语义树对应着的一棵完全语义树对应着S的所有解释。的所有解释。.证证明明: 若若不不然然，设设T中中节节点点N向向下下生生出出的的n个个节节L1，Ln的每个的每个节节Li上，都至少有一个文字上，都至少有一个文字Ai不在不在I中中由由语义树
19、语义树的定的定义义知：知：Q1 Qn是恒真公式是恒真公式,其中其中Qi表示表示Li上所有文字的合取，上所有文字的合取，i=1, , n。将。将Q1 Qn化化为为合取范式：合取范式：Q1 Qn（A1 A2 An） () ()因因为为每一个析取式中都必每一个析取式中都必须须有一个互有一个互补对补对。不妨。不妨设设A1A2,于是于是A2,A2都不在都不在I中中,这这与与I是一个解是一个解释释矛盾。矛盾。结结论论：对对S的的任任意意解解释释I，都都可可以以从从S的的完完全全语语义义树树的的根根点点出出发发，向下找出一条分枝，使，向下找出一条分枝，使该该分枝分枝对应对应着解着解释释I。引理引理设设T是子
20、句集是子句集S的完全语义树，的完全语义树，I是是S的一个解的一个解释。于是释。于是T中任意节点向下生出的直接节中，必中任意节点向下生出的直接节中，必有一节，其上所有文字都在有一节，其上所有文字都在I中。中。.子句集的封闭语义树子句集的封闭语义树l定义（失效点）定义（失效点）称语义树称语义树T中的节点中的节点N为失效为失效点，如果点，如果(1)I(N)弄假弄假S中某个子句的某个基例；中某个子句的某个基例；(2)I(N)不弄假不弄假S中任意子句的任意基例，其中中任意子句的任意基例，其中N是是N的任意祖先节点。的任意祖先节点。l定义（封闭语义树）定义（封闭语义树）语义树语义树T是封闭的，当且是封闭的
21、，当且仅当仅当T的每的每个分枝的终点都是失效点。个分枝的终点都是失效点。l定义（推理点）定义（推理点）称封闭语义树的节点称封闭语义树的节点N为推理为推理点，如果点，如果N的所有直接下降节点都是失效点的所有直接下降节点都是失效点.例例.设设S=P,P R,P Q,P R。S的原子集A=P,Q,RPPQQQQRRRRRRRRPPQQRR.练习练习l设子句集S=P(x)Q(x),P(f(x),Q(f(x)分别画出S的完全语义树与封闭语义树。.二、二、Herbrand定理定理Herbrand定定理理I子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义树证证明明: 必要性：
22、若S是不可满足的，设T是S的完全语义树对T的每一个分枝B,令IB是附着在B上所有文字的集合，则IB是S的一个解释,故IB弄假S中某子句C的某个基例C由于C是有限的，所以B上存在一个节点NB使得部分解释I（NB）弄假C，于是分枝B上存在失效点因此，对T中每一分枝都存在一个失效点，于是从T得到S的一个封闭语义树T。.Herbrand定理定理I子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义树(有限性)因为封闭语义树T中每一个节点只能向下生长有限个节,故T必有有限个节点.否则,由Konig无限性引理,T中必有一条无穷的分枝,此无穷分枝上当然没有失效点,矛盾。（Koni
23、g无限性引理：在一个其点之次数有限的无限有向树中，必有一源于根的无限路。）充分性：若S的每一个完全语义树T都对应着一个有限封闭语义树T，则T的每条分枝上都有一个失效点。因为S的任一解释都对应T的某一条分枝，所以每一个解释都弄假S，故S是不可满足的。.Herbrand定理定理II 子句集S是不可满足的，当且仅当存在S的一个有限不可满足的S的基例集S。证明证明: 必要性：必要性：若若S恒假，设恒假，设T是是S的完全语义树，由的完全语义树，由Herbrand定理定理I知，有一个有限封闭知，有一个有限封闭语义树语义树 T对应着对应着T。令令S是被是被 T中所有失效点弄假的所有中所有失效点弄假的所有基例
24、（基例（S中某些子句的基例）的集合。中某些子句的基例）的集合。因为因为T中失效点的个数有限，所以中失效点的个数有限，所以S是有限集合。是有限集合。任取任取S的一解释的一解释I，则，则I是是S的某个解的某个解释释I的子集，而解释的子集，而解释I是是T中一个分中一个分枝，所以，枝，所以，I弄假弄假S中子句中子句C，故，故I弄弄假假S。因因为为I I,且且I是是S的的解解释释,故故I弄弄假假S由由I的的任任意意性性知知S不不可可满满足。足。 S=P(x),P(a)P(b),Q(f(x)H=a,b,f(a),f(b),f(f(a),f(f(b),A=P(a),P(b),Q(a),Q(b),S=P(a)
25、,P(b),P(a)P(b).Herbrand定理定理II 子句集S是不可满足的，当且仅当存在S的一个有限不可满足的S的基例集S。充分性：充分性：假设假设S有一个有限的不可满足的基例集有一个有限的不可满足的基例集S。 任取任取S的解释的解释I， 因因为为S的的每每一一个个解解释释I都都包包含含着着S的的一一个个解解释释I，而而S是是不不可可满满足足的的，所所以以S的的任任一一解解释释I都都弄弄假假S，故故I弄弄假假S中中至至少少一一个个子子句句，即即I弄弄假假S中中至至少少一个子句的基例，亦即一个子句的基例，亦即I弄假弄假S。 由由I的任意性，知的任意性，知S是不可满足的。是不可满足的。.He
26、rbrand定理II提出了一种证明子句集S的不可满足性的方法：如果存在这样一个机械程序，它可以逐次生成S中子句的基例集S0，Sn，并逐次地检查S0，Sn，的不可满足性，那么根据Herbrand定理，如果S是不可满足的，则这个程序一定可以找到一个有限数N，使SN是不可满足的。.使用使用Herbrand定理的机器证明过程定理的机器证明过程lGilmore过程lD-P过程.Gilmore过程（过程（1960年）年）l逐逐次次地地生生成成S0， S1，Sn，其其中中Si是是用用S的的i级级常常量量集集合合Hi中中的的常常量量，代代替替S中中子子句句的的变变量量，而得到的而得到的S的所有基例之集合。的所
27、有基例之集合。l对对于于每每一一个个Si，可可以以使使用用命命题题逻逻辑辑中中的的任任意意的的方法去方法去检查检查Si的不可的不可满满足性。足性。 Gilmore使使用用了了所所谓谓乘乘法法方方法法：即即将将Si化化为为析析取取范范式式。如如果果其其中中任任意意一一个个合合取取项项包包含含一一个个互互补补对对，则则可可以以删删除除这这个个合合取取项项，最最后后，如如果果某某个个Si是空的，是空的，则则Si是不可是不可满满足的。足的。l当当S不可不可满满足足时时，该该算法一定算法一定结结束束(半可判定半可判定)。.例例.S=P(a),P(x)Q(f(x),Q(f(a)H0=aS0=P(a)(P(
28、a)Q(f(a)Q(f(a)=(P(a)P(a)Q(f(a)(P(a)Q(f(a)Q(f(a)=所以，S是不可满足的。l该该算法具有指数复算法具有指数复杂杂性，性，为为此提出了改此提出了改进规则进规则，称，称为为Davis-Putnam预处预处理理-检验检验基子句集不可基子句集不可满满足性。足性。.D-P过程过程设设S是基子句集是基子句集lTautology删除规则删除规则设设S为删去为删去S中所有的中所有的Tautology所剩子句集，所剩子句集，则则S恒假恒假iffS恒假。恒假。.l单文字规则单文字规则若若S中有一个单元基子句中有一个单元基子句L，令令S为删除为删除S中包含中包含L的所有基
29、子句所剩子句集，的所有基子句所剩子句集，则：则：(1)若若S为空集，则为空集，则S可满足。可满足。(2)否则，否则，令令S为删除为删除S中所有文字中所有文字L所得子句集所得子句集（若（若S中有单元基子句中有单元基子句L，则删文字，则删文字L得空子句），得空子句），于是，于是，S恒假恒假iffS恒假。恒假。S=L(LC1)(LCi)(LCi+1)(LCj)Cj+1Cn.定义（纯文字）：称定义（纯文字）：称S的基子句中文字的基子句中文字L是纯的，如果是纯的，如果L不出现在不出现在S中。中。l纯文字规则纯文字规则设设L是是S中纯文字，且中纯文字，且S为删除为删除S中所有包含中所有包含L的基子句所的基
30、子句所剩子句集，则剩子句集，则(1)若若S为空集，则为空集，则S可满足。可满足。(2)否则，否则，S恒假恒假iffS恒假。恒假。S=(LC1)(LCi)Ci+1Cn.l分裂规则分裂规则若若S=(A1 L) (Am L) (B1 L) (Bn L) R 其中其中Ai, Bi ,R都不含都不含L或或L，令，令 S1 =A1 Am RS2=B1 Bn R 则则S恒假恒假 iffS1 ， S2同同时时恒假。恒假。 .Davis-Putnam方法练习方法练习lS=(P Q R) (P Q) P R UlS=(P Q) (P Q) (Q R) (Q R)lS=(P Q) (P Q) (R Q) (R Q)
31、.Herbrand定理的主要障碍定理的主要障碍l要求生成关于子句集要求生成关于子句集S的基例集的基例集S1,S2,。在多数情况。在多数情况下，这些集合的元数是以指数方式增加的：下，这些集合的元数是以指数方式增加的：例例.S=P(x,g(x),y,h(x,y),z,k(x,y,z),P(u,v,e(v),w,f(v,w),x) H0=a H1=a, g(a), h(a, a), k(a, a, a), e(a), f(a, a) S0=P(a,g(a),a,h(a,a),a,k(a,a,a),P(a,a,e(a),a,f(a,a),a) S1=(6 6 6)+(6 6 6 6)=216+1296
32、=1512个元素个元素 S5是是不不可可满满足足的的，但但是是H5是是1065数数量量级级个个元元素素，而而S5有有10260数数量量级级的的元元素素。想想将将S5存存储储起起来来都都是是不不可可能能的的，更不要更不要说说是是检查检查它的不可它的不可满满足性了。足性了。.l为了避免像Herbrand定理所要求的那样去生成子句的基例集，J.A.Robinson于1965年提出了归结原理，归结原理可以直接应用到任意子句集S上（不一定是基子句集），去检查S的不可满足性。l归结原理的本质思想是去检查子句集S是否包含一个空子句:如果S包含，则S是不可满足的。如果S不包含，则去检查是否可由S推导出来。当然
33、这个推理规则必须保证推出的子句是原亲本子句的逻辑结果。归结原理就是具有这种性质的一种推理规则。归结原理思想归结原理思想.命题逻辑中的归结原理命题逻辑中的归结原理.归结归结式式l定定义义（归结式）对任意两个基子句C1和C2。如果C1中存在文字L1，C2中存在文字L2，且L1L2，则从C1和C2中分别删除L1和L2，将C1和C2的剩余部分析取起来构成的子句，称为C1和C2的归结式，记为R(C1,C2)。C1和C2称为亲本子句。.练习练习:求下述各子句对的归结式求下述各子句对的归结式lC1=PQR,C2=QSlC1=PQR,C2=PRQ.定定理理设C1和C2是两个基子句，R(C1,C2)是C1，C2
34、的归结式，则R(C1,C2)是C1和C2的逻辑结果。证证明：明：设C1=LC1,C2=LC2。于是R(C1,C2)C1C2设I是C1和C2的一个解释，且满足C1也满足C2。因为L和L中有一个在I下为假，不妨设为L。于是C1非空，且在I下为真。故R(C1,C2)在I下为真。命题逻辑归结方法的可靠性命题逻辑归结方法的可靠性.归结演绎归结演绎l定定义义（归归结结演演绎绎） 设设S是是子子句句集集。从从S推推出出子子句句C的的一一个个归归结结演演绎绎是如下一个有限子句序列：是如下一个有限子句序列： C1，C2，Ck其中其中Ci或者是或者是S中子句，或者是中子句，或者是Cj和和Cr的的归结归结式式 (j
35、 i, r i)；并且并且CkC。 称从子句集称从子句集S演演绎绎出子句出子句C，是指存在一个从，是指存在一个从S推出推出C的演的演绎绎。l定理定理 若从子句集若从子句集S可以演可以演绎绎出子句出子句C，则则C是是S的的逻辑结逻辑结果。果。l推推论论 若子句集若子句集S是可是可满满足的，足的， 则则S推出的任意子句也是可推出的任意子句也是可满满足的。足的。 .定定义义 从从S推推出出空空子子句句的的演演绎绎称称为为一一个个反反驳驳（反反证证） ，或称，或称为为S的一个的一个证证明。明。结结论论：若若从从基基子子句句集集S可可演演绎绎出出空空子子句句，则则S是是不不可可满满足的。足的。演演绎绎树
36、树：从从子子句句集集S出出发发，通通过过归归结结原原理理可可得得到到一一个个向向下下的的演演绎绎树树，其其每每个个初初始始节节点点上上附附着着一一个个S中中子子句句，每每个个非非初初始始节节点点上上附附着着一一个个其其前前任任节节点上子句的点上子句的归结归结式。式。.例.S=P Q, P Q, P Q, P Q 归结演绎：(1)PQ(2)PQ(3)PQ(4)PQ(5)Q由(1)、(2)(6)Q由(3)、(4)(7)由(5)、(6).归结原理归结原理一般过程一般过程:1)建立子句集S。2)如果S含空子句，则结束。3)从子句集S出发,仅对S的子句间使用归结推理规则。4)如果得出空子句，则结束。5)
37、将所得归结式仍放入S中。6)对新的子句集使用归结推理规则。转4)。.例例.证明证明(PQ) Qp首先建立子句集:S=PQ,Q,P归结演绎:(1)PQ(2)Q(3)P(4)P(1)(2)归结(5)(3)(4)归结.命题逻辑归结原理的完备性命题逻辑归结原理的完备性l定理如果基子句集如果基子句集S是不可满足的，是不可满足的，则存在从则存在从S推出空子句的归结演绎。推出空子句的归结演绎。证明：设M是S的原子集，对M的元素数|M|用归纳法。当|M|=1时，设原子为P。若S，得证。否则，因为S是不可满足的，于是，S中必包含单元子句P和P，而P和P的归结式是，所以存在从S推出的归结演绎。假设|M|n(n2)
38、时，定理成立。往证|M|n时定理成立。.取取M中任意一原子中任意一原子P，做如下两个子句集：，做如下两个子句集：S：将：将S中所有含中所有含P的子句的子句删删除，然后在剩下的子除，然后在剩下的子 句中句中删删除文字除文字P；S”：将：将S中所有含中所有含P的子句的子句删删除，然后在剩下的除，然后在剩下的 子句中子句中删删除文字除文字P。显显然，然，S和和S”都不可都不可满满足，且它足，且它们们的原子集的元的原子集的元素数都小于素数都小于n。根据。根据归纳归纳假假设设，存在从，存在从S推出推出 的的归结归结演演绎绎D1，从，从S”推出推出 的的归结归结演演绎绎D2。.lS=PC1,PCi,PCi
39、+1,PCj,Cj+1,CnS=Ci+1,Cj,Cj+1,CnS=C1,Ci,Cj+1,Cnl例：S=P Q, P Q, P R, RM=P,Q,R. 在在D1中，将中，将S中所有不是中所有不是S中的子句，通中的子句，通过过添加文字添加文字P而恢复成而恢复成S中子句，于是，得到从中子句，于是，得到从S推出推出 或者或者P的的归结归结演演绎绎D1。 用同用同样样方法从方法从D2可得一个从可得一个从S推出推出 或者或者P的的归结归结演演绎绎D2。 显显然，从然，从D1和和D2就不就不难难得到一个从得到一个从S推出推出 的的归结归结演演绎绎D。归纳归纳法完成。法完成。.ResolutionPrinc
40、iple两种译法：归结原理：从内部看刘叙华，一种新的语义归结原理，吉林大学学报，1978。消解原理：从外部看马希文，机器证明及其应用，计算机应用，1978。.6.3 合一算法合一算法.例例1C1：P(x) Q(y)C2：P(a) R(z)例例2C1：P(x) Q(x)C2：P(f(x) R(x)l替换和合一是为了处理谓词逻辑中子句之间的模式匹配而引进.一、替换与最一般合一替换一、替换与最一般合一替换l定定义义(替替换换)一一个个替替换换是是形形如如t1/v1, , tn/vn 的的一一个个有有限限集集合合，其其中中vi是是变变量量符符号号，ti是是不不同同于于vi的的项项。并并且且在在此此集集
41、合合中中没没有有在在斜斜线线符符号号后后面面有有相相同同变变量量符符号号的的两两个个元元素素，称称ti为为替替换换的分子，的分子，vi为为替替换换的分母。的分母。例例. a/x, g(y)/y, f(g(b)/z是替是替换换; x/x, y/f(x), a/x, g(y)/y, f(g(b)/y不是替不是替换换;基替基替换换:当当t1,tn是基是基项时项时，称此替，称此替换为换为基替基替换换。空替空替换换：没有元素的替没有元素的替换换称称为为空替空替换换，记为记为 。.替换定定义义（改名）（改名） 设设替替换换 = t1/x1, , tn/xn 如果如果t1, , tn是不同的是不同的变变量符
42、号，量符号，则则称称 为为一个改一个改名替名替换换，简简称改名。称改名。替换作用对象：替换作用对象：表达式表达式（项、项集、原子、原子集、（项、项集、原子、原子集、文字、子句、子句集）文字、子句、子句集）基表达式：基表达式：没有变量符号的表达式。没有变量符号的表达式。子表达式：子表达式：出现在表达式出现在表达式E中的表达式称为中的表达式称为E的子的子表达式。表达式。.E的例l定定义义（E的的例例） 设设 = t1/v1, , tn/vn 是是一一个个替替换换，E是是一一个个表表达达式式。将将E中中出出现现的的每每一一个个变变量量符符号号，vi (1 i n) ，都都用用项项ti替替换换，这这样
43、样得到的表达式得到的表达式记为记为E 。称。称E 为为E的例。的例。 若若E 不含不含变变量，量，则则E 为为E的基例。的基例。例例. 令令 = a/x, f(b)/y, c/z，E=P(x, y, z)于是于是E的例（也是的例（也是E的基例）的基例）为为 E = P(a, f(b), c).练习：lE=P(x,g(y),h(x,z),=a/x,f(b)/y,g(w)/zE=P(a,g(f(b),h(a,g(w)lE=P(x,y,z),=y/x,z/yE=P(y,z,z).EP(z,z,z).替换的乘积替换的乘积l定定义义（替替换换的的乘乘积积）设设 = t1/x1, , tn/xn ， =
44、u1/y1, , um/ym 是两个替是两个替换换。将下面集合。将下面集合 t1 /x1, , tn /xn , u1/y1, , um/ym 中任意符合下面条件的元素中任意符合下面条件的元素删删除：除： 1）ui/yi，当，当yi x1, , xn 时时； 2）ti /xi，当，当ti = xi 时时。如此得到一个替如此得到一个替换换，称，称为为 与与 的乘的乘积积，记为记为 。l例例. 令令 =f(y)/x, z/y =a/x, b/y, y/z 于是得集合于是得集合 t1 /x1, t2 /x2 , u1/y1, u2/y2 , u3/y3 = f(b)/x, y/y, a/x, b/y
45、, y/z 与与 的乘的乘积为积为 = f(b)/x, y/z .=a/x,=b/x =a/x =b/x可见： .例子例子:E=P(x,y,z) =a/x,f(z)/y,w/zE =P(a,f(z),w) =t/z,g(b)/w(E ) =P(a,f(t),g(b) =a/x,f(t)/y,g(b)/z,g(b)/wE=P(a,f(t),g(b).引理引理 若若E是表达式，是表达式， ， 是两个替是两个替换换， 则则E ( ) = (E ) 证证明：明： 设设vi是是E中任意一个中任意一个变变量符号，而量符号，而 = t1/x1, , tn/xn ， = u1/y1, , um/ym l若若v
46、i既既不不在在 x1, , xn 中中，也也不不在在 y1, , ym 中中，则则vi在在E ( )中和在中和在(E ) 中都不中都不变变。l若若vi=xj (1 j n)，则则E中中的的vi，在在(E ) 中中先先变变成成tj，然然后后再再变变成成tj ；E中中的的vi在在E()中中立立即即就就变变成成了了tj 。故故E中中vi在在(E ) 中和在中和在E()中有相同中有相同变变化。化。l若若vi=yj (1 j m)，且且yj x1,xn ，则则E中中vi在在(E ) 中中变变为为uj;E中中vi在在E()中中也也变变为为uj(注注意意:yj x1, xn，所所以以uj/yj），故故E中中
47、vi在在(E ) 中中和和在在E ()中中有有相同相同变变化。化。 由于由于vi的任意性，故引理得的任意性，故引理得证证。.引理引理 设设 ， ， 是三个替是三个替换换， 于是于是() ()证证明：明： 设设E是任一表达式，由上面引理知是任一表达式，由上面引理知 E() =(E() = (E ) ) E( () =(E ) () = (E ) ) 所以所以 E() = E( ()由于由于E的任意性，故的任意性，故 () ().l定定义义(合合一一)称称替替换换 是是表表达达式式集集合合E1,Ek的的 合一，当且合一，当且仅仅当当E1 E2 =Ek 。 表表达达式式集集合合E1, , Ek称称为
48、为可可合合一一的的，如如果存在关于此集合的一个合一。果存在关于此集合的一个合一。l定定义义(最最一一般般合合一一) 表表达达式式集集合合E1, , Ek的的合合一一 称称为为是是最最一一般般合合一一(most general unifier, 简简写写为为mgu)，当当且且仅仅当当对对此此集集合合的的每每一个合一一个合一 ，都存在替，都存在替换换 ，使得，使得 .l例例.表达式集合P(a,y),P(x,f(b)是可合一的，其最一般合一a/x,f(b)/y。显然，这也是此集合的mgu。？表达式集合P(a,b),P(x,f(b)是否可合一？l例例.表达式集合P(x),P(f(y)是可合一的，其最一
49、般合一f(y)/xf(a)/x,a/y也是合一，有替换=a/y，使=f(y)/xa/y.l例例S=P(x) Q(x),P(y),Q(b)P(x),P(y)可合一，可合一， a/x,a/y是合一，是合一，其其mgu x/y，有替换，有替换 =a/x，使，使 =x/y a/x.二、二、合一算法合一算法定定义义（差差异异集集合合）设W是非空表达式集合，W的差异集合是如下一个集合：首先找出W的所有表达式中不是都相同的第一个符号，然后从W的每一个表达式中抽出占有这个符号位置的子表达式。所有这些子表达式组成的集合称为这步找到的W的差异集合D。.W不可合一的三种情况不可合一的三种情况（1）若D中无变量符号为
50、元素，则W是不可合一的。l例例.W=P(f(x),P(g(x)D=f(x),g(x)（2）若D中有奇异元素和非奇异元素，则W是不可合一的。l例例.W=P(x),P(x,y)D=,y（3）若D中元素有变量符号x和项t，且x出现在t中，则W是不可合一的。l例例.W=P(x),P(f(x)D=x,f(x).l换名换名:P(f(x),x),P(x,a);如果不换名：D=f(x),x.换名:P(f(y),y),P(x,a);mgu:f(a)/x,a/y.步骤1：置k=0,Wk=W,k=步骤2：若Wk只有一个元素，则停止，k是W的最一般合一；否则，找出Wk的差异集合Dk。步骤3：若Dk非奇异，Dk中存在元
51、素vk和tk，其中vk是变量符号，并且不出现在tk中，则转步骤4；否则，算法停止，W是不可合一的。步骤4：令k+1=ktk/vk，Wk+1=Wk（注：Wk+1=W）步骤5：置k=k+1，转步骤2。合一算法（合一算法（Unificationalgorithm）.例例.令W=Q(f(a),g(x),Q(y,y),求W的mgu。l步骤1：k=0,W0=W,0=。l步骤2：D0=f(a),y。l步骤3：有v0=yD0，v0不出现在t0f(a)中。l步骤4：令1=0t0/v0=f(a)/y,W1=Q(f(a),g(x),Q(f(a),f(a)l步骤5：k=k+1=1l步骤2：D1=g(x),f(a)。l
52、步骤3：D1中无变量符号，算法停止，W不可合一。？若令W=Q(f(a), g(x), Q(y, z), W是否可合一？.例例令令 W= P(a, x, f(g(y), P(z, f(z), f(u)， 求出求出W的的mgu。步骤1：k=0,W0=W,0=。步骤2：D0=a,z。步骤3：有v0=zD0，v0不出现在t0a中。步骤4：令1=0t0/v0=a/z=a/z，W1=W0t0/v0=P(a,x,f(g(y),P(z,f(z),f(u)a/z=P(a,x,f(g(y),P(a,f(a),f(u)步骤5：k=k+1=1步骤2：D1=x,f(a)。步骤3：有v1=xD1，且v1不出现在t1f(a
53、)中。步骤4：令2=1t1/v1=a/zf(a)/x=a/z,f(a)/x，W2=W1t1/v1=P(a,x,f(g(y),P(a,f(a),f(u)f(a)/x=P(a,f(a),f(g(y),P(a,f(a),f(u).例例.步步骤骤5：k=k+1=2步步骤骤2： D2 =g(y), u。步步骤骤3：有：有v2=u D2，且，且v2不出不出现现在在t2g(y)中。中。步步骤骤4：令：令 3= 2 t2/v2=a/z, f(a)/x g(y)/u =a/z, f(a)/x, g(y)/u ，W3=W2t2/v2=P(a, f(a), f(g(y), P(a, f(a), f(u) g(y)/
54、u =P(a, f(a), f(g(y)步步骤骤5:k=k+1=3步步骤骤2：W3只有一个元素。算法停止。只有一个元素。算法停止。 3=a/z, f(a)/x, g(y)/u 是是W的最一般合一。的最一般合一。.定理定理 若若W是关于表达式的是关于表达式的有限非空可合一有限非空可合一集合，集合，则则合一合一算法算法终终将将结结束在步束在步骤骤2，并且最后的，并且最后的 k是是W的最一般合一。的最一般合一。证明：（1）终止性。否则将产生一个无穷序列：W，W，W，其中每一个直接后继集合比它的前任都少一个变量符号（注意：W包含vk，而W不包含vk）。但这是不可能的，因为W仅含有限个变量符号。（2）k
55、是W的合一。若算法停止在步骤2，则Wk=W只含有一个元素，所以k是W的合一。.（3）用用归归纳纳法法证证明明算算法法必必不不会会停停止止在在步步骤骤3，并并且且对对任任意意W的的一一个个合合一一 ，任任意意k，都都存存在在替替换换 k，使得，使得 = k k 亦即亦即 k是是W的的mgu。 当当k=0时时，因，因 0= ，取，取 0= ，于是，于是 = 0 0。.假假设对设对0 k n， = k k成立。成立。 往往证证：存在：存在 n+1，使得，使得 = n+1 n+1。若若W 只含有一个元素，只含有一个元素，则则合一算法合一算法结结束在步束在步骤骤2。因。因为为 = n n，且，且 n是是
56、W的合一，故的合一，故 n是是W的的mgu。定理得。定理得证证。若若W 不只含有一个元素不只含有一个元素,按照算法按照算法,将找出将找出W的差异集合的差异集合Dn。因因为为 = n n是是W的合一，所以的合一，所以W中表达式中表达式经经替替换换 作用后都作用后都变变成同一个相同的表达式。而成同一个相同的表达式。而W中表达式中表达式经经 n作用后，作用后，产产生了差异集合生了差异集合Dn，所以，所以Dn必必须须被被 n所所统统一，即一，即 n是是D n的合的合一。一。. 因因为为Dn是是可可合合一一的的（ n就就是是Dn的的合合一一），所所以以必必有有变变量量符符号号vn Dn；Dn中中至至少少
57、有有两两个个不不同同元元素素。所所以以可可设设tn Dn，且且tnvn。显显然然，变变量量符符号号vn不不出出现现在在tn中中（否否则则，vn n tn n，这这与与 n是是Dn的合一矛盾）。的合一矛盾）。 因因此此算算法法不不能能停停止止在在步步骤骤3，所所以以算算法法必必然然停停止在步止在步骤骤2。.令令 n+1= n tn/vn。因。因为为vn n=tn n,所以所以tn n/vnn令令 n+1= n -tn n/vn。因。因vn不出不出现现在在tn中，所以中，所以于是于是 故故归归纳纳法法完完成成。即即对对所所有有k0,都都存存在在替替换换 k，使使 = k k。所所以以算算法法终终止
58、止步步骤骤2时时， k是是W的的最最一般合一。一般合一。.6.4一阶逻辑中的归结原理一阶逻辑中的归结原理.定定义义（因因子子） 如如果果子子句句C中中，两两个个或或两两个个以以上上的的文文字有一个最一般合一字有一个最一般合一 ，则则C 称称为为C的因子；的因子； 如果如果C 是是单单元子句，元子句，则则C 称称为为C的的单单因子。因子。例例. C=P(x) P(f(y) Q(x) 令令 f(y)/x，于是，于是 C = P(f(y) Q(f(y) 是是C的因子。的因子。.二元归结式定定义义 设设C1, C2是两个是两个无公共无公共变变量量的子句的子句(称称为亲为亲本子句本子句), L1, L2
59、分分别别是是C1, C2中的两个文字。中的两个文字。 如果如果L1和和L2有最一般合一有最一般合一 ，则则子句子句 (C1 - L1 ) ( C2 - L2 ) 称称为为C1和和C2的二元的二元归结归结式，式，L1和和L2称称为归结为归结文字。文字。例例. 设设C1=P(x) Q(x), C2=P(a) R(x)将将C2中中x改名改名为为y。取。取L1P(x), L2=P(a), =a/x, 于是于是(C1 - L1 ) ( C2 - L2 )(P(a), Q(a)-P(a) (P(a), R(y)-P(a)=Q(a), R(y)= Q(a) R(y) -C1和和C2的二元的二元归结归结式式.
60、练习练习：设设C1=P(a) R(x), C2=P(y) Q(b) 求求C1和和C2的二元的二元归结归结式式.在在谓词逻辑谓词逻辑中，中，对对子句子句进进行行归结归结推理推理时时，要注意，要注意的几个的几个问题问题：（1）若若被被归归结结的的子子句句C1 和和C2中中具具有有相相同同的的变变元元时时，需需要要将将其其中中一一个个子子句句的的变变元元更更名名，否否则则可可能能无无法法合合一一，从而没有从而没有办办法法进进行行归结归结。 .l例：例： C1=P(x), C2=P(f(x) l例：例：设设知知识库识库中有如下知中有如下知识识：(1)若若x的父的父亲亲是是y，则则x不是女人。不是女人。
61、(2)若若x的母的母亲亲是是y，则则x是女人。是女人。(3)Chris的母的母亲亲是是Mary。(4)Chris的父的父亲亲是是Bill。求求证证：这这些断言包含有矛盾。些断言包含有矛盾。 father(x,y):x的父的父亲亲是是y mother(x,y):x的母的母亲亲是是y woman(x):x是女人是女人.（2）在在求求归归结结式式时时,不不能能同同时时消消去去两两个个互互补补文文字字对对,消消去去两两个个互互补补文字文字对对所得的所得的结结果不是两个果不是两个亲亲本子句的本子句的逻辑逻辑推推论论。例例.设设C1=P(x) Q(b), C2=P(a) Q(y) R(z) 求求C1和和C
62、2的二元的二元归结归结式式.（3）如如果果在在参参加加归归结结的的子子句句内内含含有有可可合合一一的的文文字字,则则在在进进行行归归结结之之前前,应应对对这这些些文文字字进进行行合合一一,以以实实现现这这些些子子句句内内部部的的化化简简。 .归结归结式式定定义义 子句子句C1, C2的一个的一个归结归结式是下列二元式是下列二元归结归结式之一：式之一：(1)C1和和C2的二元的二元归结归结式。式。(2)C1和和C2的因子的二元的因子的二元归结归结式。式。(3)C1的因子和的因子和C2的二元的二元归结归结式。式。(4)C1的因子和的因子和C2的因子的二元的因子的二元归结归结式。式。例例. 设设 C
63、1=P(x) P(f(y) R(g(y) C2=P(f(g(a) Q(b)C1的的因因子子C1= P(f(y) R(g(y)。于于是是C1和和C2的的二二元元归归结结式，从而也是式，从而也是C1和和C2的的归结归结式式为为 R(g(g(a) Q(b).一一阶逻辑归结阶逻辑归结原理的完原理的完备备性性提升引理提升引理如果C1和C2分别是子句C1和C2的例，C是C1和C2的归结式，则存在C1和C2的一个归结式C，使C是C的例。例C1：P(x) Q(f(x) C2：Q(y) R(y)C1：P(a) Q(f(a) C2：Q(f(a) R(f(a) C：P(a) R(f(a) C：P(x) R(f(x)
64、 .一一阶逻辑归结阶逻辑归结原理的完原理的完备备性性l定理定理若子句集若子句集S是不可满足的，则存在从是不可满足的，则存在从S推推出空子句的归结演绎。出空子句的归结演绎。证明证明:设子句集设子句集S是不可满足的，由是不可满足的，由Herbrand定定理理II知，存在知，存在S的一个基例集的一个基例集S也是不可满足的。也是不可满足的。根据命题根据命题逻辑归结逻辑归结原理的完原理的完备备性性，存在从，存在从S推推出空子句的归结演绎出空子句的归结演绎D。由提升引理知，可将由提升引理知，可将D提升成一个从提升成一个从S推出空推出空子句的归结演绎子句的归结演绎D。定理得证。定理得证。 .应用归结原理的习
65、题应用归结原理的习题.6.5归结原理的几种改进归结原理的几种改进.l水平浸透法（水平浸透法（LevelSaturationMethod）S0=SSn=C1和和C2的归结式的归结式|C1S0Sn-1，C2Sn-1.例.使用水平浸透法证明S=PQ,PQ,PQ,PQ不可满足。S0:(1)P Q(2)P Q(3)P Q(4)P QS1:(5)Q由由(1),(2)(6)P由由(1),(3)(7)Q Q由由(1),(4)(8)P P由由(1),(4)(9)Q Q由由(2),(3)(10)P P由由(2),(3)(11)P由由(2),(4)(12)Q由由(3),(4)S2:(13)P Q由由(1),(7)(
66、14)P Q由由(1),(8)(15)P Q由由(1),(9)(16)P Q由由(1),(10)(39) 由由(5),(12).l水平浸透法的特点：水平浸透法的特点：完备完备l水平浸透法的问题：水平浸透法的问题：无控制的盲目归结导致大量无用子句产生无控制的盲目归结导致大量无用子句产生-对于大一些的问题，在产生空子句前可能就产生了组对于大一些的问题，在产生空子句前可能就产生了组合爆炸合爆炸l改进思想：改进思想：寻找控制策略，使之合理地选取亲本子句，尽可能地寻找控制策略，使之合理地选取亲本子句，尽可能地减小归结的盲目性，使其尽快归结出空子句。减小归结的盲目性，使其尽快归结出空子句。.一、支架集归结
67、一、支架集归结1965,L.Wos,J.A.Robinson,D.F.Carson.J.ACM12(4):536-541.定义子句集定义子句集S的子集的子集T称为称为S的支架集，如果（的支架集，如果（S-T）是可满足的。一个）是可满足的。一个支架集归结是一个不同时属于（支架集归结是一个不同时属于（S-T）的两个子句的归结。）的两个子句的归结。例例.设设S是如下子句集：是如下子句集：(1)P Q(2)P Q(3)P Q(4)P Q令令T=P Q，显然，显然T是支架集。如下的演绎是支架集归结演绎：是支架集。如下的演绎是支架集归结演绎：(5)P由由(1)、(2)(6)Q由由(1)、(3)(7)Q由由
68、(5)、(4)(8) 由由(6)、(7).l 支架集归结的完备性支架集归结的完备性若若S是有限不可满足的子句集，是有限不可满足的子句集，T是是S的支架集，的支架集，则存在从则存在从S推出空子句的支架集演绎。推出空子句的支架集演绎。.l练习：练习：设有如下子句集：设有如下子句集： S=I(x)R(x), I(a), R(y)L(y), L(a)(1)使用水平浸透法证明使用水平浸透法证明S不可满足。不可满足。(2)设支架集设支架集T=I(x)R(x)，写出从，写出从S推出空子句的支架集演绎推出空子句的支架集演绎（用支架集归结法证明（用支架集归结法证明S不可满足）。不可满足）。.二、语义归结二、语义
69、归结1967, J.R.Slagle.J.ACM 14(4):687-697.l例例.S=P Q R,P R,Q R,R，用水平浸透法证明用水平浸透法证明S的不可满足性。的不可满足性。S0:(1)P Q R(2)P R(3)Q R(4)RS1:(5)Q R由由(1),(2)(6)P R由由(1),(3)(7)P Q由由(1),(4)(8)P由由(2),(4)(9)Q由由(3),(4)S3:(23) .l想法一想法一 用子句集用子句集S的语义解释将的语义解释将S分成两部分分成两部分S1,S2，要求同一部分里的子，要求同一部分里的子句不允许进行归结，这样就阻止了很多无用子句的产生。句不允许进行归结
70、，这样就阻止了很多无用子句的产生。S1：S中被中被I弄假的子句组成的集合；弄假的子句组成的集合；S2：S中被中被I满足的子句组成的集合。满足的子句组成的集合。上例：上例： 若取若取I=P,Q,R, (S:(1)P Q R(2)P R(3)Q R(4)R) 则则 S1=(2),(3) ， S2=(1),(4) 阻止了阻止了(1),(4)的归结。的归结。.l想法二想法二 使用谓词符号的顺序，要求使用谓词符号的顺序，要求S1中的子句的归结中的子句的归结文字是该子句中最大谓词符号。文字是该子句中最大谓词符号。上例：上例： 若令若令PQR, 则阻止了则阻止了(2),(4)之间及之间及 (3),(4)之间
71、的归结。之间的归结。.l将上面两种思想用于上例：(1)P Q R(2)P R(3)Q R(4)R令令I=P,Q,R,PQR，(5)Q R由由(1),(2)(6)P R由由(1),(3)S2=(1),(4),(5),(6)(7)R由由(3),(5)(8)R由由(2),(6)S1=(2),(3),(7),(8)(9) 由由(4),(7)由由(1),(2),(3)产生产生R，集团归结的思想，集团归结的思想-想法三想法三为了当集团中子句无论以什么次序去归结，最后得到的子句是相同的。为了当集团中子句无论以什么次序去归结，最后得到的子句是相同的。.定定义义（语语义义互互撞撞clash） 设设I是是子子句句
72、集集S的的一一个个解解释释，P是是S中中谓谓词词符符号号的的一一个个顺顺序序，有有限限子子句句序序列列 (E1,Eq,N) (q 1)称称为为关关于于P和和I的的语语义义互互撞撞（简简称称PI-互互撞撞），当当且且仅仅当当E1, , Eq, N 满满足下面条件：足下面条件：(1)E1, , Eq在在I下下为为假；假；(E1, , Eq称称为该为该互撞的互撞的电电子子)(2)令令R1=N（该该互互撞撞的的核核），对对每每个个 i=1, ,q，存存在在Ri和和Ei的的归归结结式式Ri+1。(3)Ei中的中的归结归结文字是文字是Ei中最大中最大谓词谓词符号。符号。(4)Rq+1在在I下下为为假。假。
73、于是，于是，Rq+1称称为为此此PI-互撞的互撞的PI-归结归结式。式。.lPI演绎：从S出发的一个演绎称为PI演绎，当且仅当演绎中的每一个子句或是S中子句，或是一个PI-归结式。.上例上例. (1)PQR(2)PR(3)QR(4)R令令 I=P, Q, R，P Q R。于是在。于是在I下为假的子句只有两个：下为假的子句只有两个：PR, QR可得如下可得如下PI-演绎：演绎：(5)R 由由(2)、(3) 、(1)(6) 由由(5)、(4).l语义归结的完备性语义归结的完备性若若S是有限不可满足的子句集，是有限不可满足的子句集，P是是S中谓词符号的一个次序，中谓词符号的一个次序，I是是S的一个解
74、释，的一个解释，则存在从则存在从S推出空子句的推出空子句的PI演绎。演绎。.三、线性归结三、线性归结1970,D.W.Loveland,Proc.IRIA,147-162;D.Luckham,Proc.IRIA,163-190.l定义（线性归结演绎）定义（线性归结演绎）设设S是一个子句集，是一个子句集，C0是是S中的一个子句。以中的一个子句。以C0为顶为顶子句，从子句，从S到到Cn的的线线性性归结归结演演绎绎是如下一个演是如下一个演绎绎：(1)对对于于 i=0, 1, ,n-1，Ci+1是是Ci和和Bi的的归结归结式。式。(2)每个每个Bi或者属于或者属于S，或者是一个，或者是一个Cj，其中，
75、其中j i。结论结论：线线性性归结归结完完备备。.l练习：练习：设设S=P Q,P Q,P Q,P Q，请给出从请给出从S推出空子句的线性归结演绎。推出空子句的线性归结演绎。.四、输入归结四、输入归结1970,C.L.Chang,R.C.T.Lee,J.ACM.SymbolicLogicandMechanicalTheoremProving,Academic,Press,1973.l定义：边子句都属于定义：边子句都属于S的线性归结演绎称为输的线性归结演绎称为输入归结演绎入归结演绎.l练习：练习：设有如下子句集：设有如下子句集： S=I(x)R(x), I(a), R(y)L(y), L(a)请
76、用输入归结方法证明请用输入归结方法证明S不可满足。不可满足。l结论：输入归结在结论：输入归结在Horn集集上完备。上完备。.五、单元归结五、单元归结1964,L.Wos,D.Carson,G.A.Robinson,Proc.AFIPS,616-621.l定义：若进行归结的两个亲本子句中，有一定义：若进行归结的两个亲本子句中，有一个是单元子句或者是一个子句的单元因子，个是单元子句或者是一个子句的单元因子，则称这种归结为单元归结。则称这种归结为单元归结。l练习：练习：设有如下子句集：设有如下子句集： S=I(x)R(x), I(a), R(y)L(y), L(a)请用单元归结方法证明请用单元归结方
77、法证明S不可满足。不可满足。.l结论结论1：单元归结对：单元归结对Horn子句集完备。子句集完备。（1974,L.Henschen,L.Wos,J.ACM,21(4):590-605）l结论结论2（输入归结与单元归结的等价性）：（输入归结与单元归结的等价性）：存在从子句集存在从子句集S推出空子句的充要条件推出空子句的充要条件是存在从是存在从S推出空子句的输入演绎。推出空子句的输入演绎。 (1970,C.L.Chang,J.ACM,17(4):698-701.).六、锁归结六、锁归结1971,Boyerl定定义义 设设C是是子子句句，若若将将C中中每每一一个个文文字字都都附附上上一一个个整整数，
78、数，则则称子句称子句C已配已配锁锁。这这些整数称些整数称为这为这些文字的些文字的锁锁。l定定义义 如如果果已已配配锁锁子子句句C中中有有多多于于一一个个的的相相同同文文字字，则则保保存存这这些些文文字字中中有有最最小小锁锁的的一一个个，而而将将其其余余的的删删除除。这这种作法称种作法称为为配配锁锁子句中关于相同文字的合并子句中关于相同文字的合并规则规则。l定定义义 设设C1和和C2是是两两个个配配锁锁子子句句，R(C1, C2)是是C1和和C2的的归归结结式式，如如果果C1和和C2中中的的归归结结文文字字分分别别是是C1和和C2中中带带有最小有最小锁锁的文字，的文字，则则称称R(C1, C2)
79、为为C1和和C2 的的锁归结锁归结式。式。.例例. 设设S是如下配是如下配锁锁子句集子句集(1)1P2Q(2)3P4Q(3)6P5Q(4)8P7Q于是，从于是，从S推出的推出的锁锁演演绎绎如下：如下：(5) 6P 由由 (3)、(4)(6) 2Q 由由(1)、(5)(7) 4Q 由由(2)、(5)(8) 8P 由由(6)、(4)(9) 6P 由由(3)、(7)(10) 由由(6)、(7)l结论结论：锁归结锁归结完完备备设设S是已配是已配锁锁子句集。若子句集。若S是不可是不可满满足的，足的，则则存在从存在从S推出空子句的推出空子句的锁锁演演绎绎。.归结方法间相容性问题归结方法间相容性问题l锁语义
80、归结锁语义归结1978,刘叙华刘叙华1型型IDI，2型型IDI完备完备l线性语义归结线性语义归结1980，刘叙华，刘叙华反例反例不完备不完备例例.S=P，Q,A P,B Q,A B，I=P,Q,A,BPQAB.l线性锁线性锁不完备不完备1989,杨玉普，线性半锁完备杨玉普，线性半锁完备例例.设设S=1P 2Q，3P4Q，5P6Q，7P 8Ql输入锁输入锁不完备不完备1984，刘叙华，输入半锁对，刘叙华，输入半锁对Horn集完备集完备l单元锁单元锁不完备不完备单元锁在单元锁在Horn集上不完备。集上不完备。1987，杨凤杰，刘叙华：若满足一定配锁条件，则单元，杨凤杰，刘叙华：若满足一定配锁条件，
81、则单元锁归结在锁归结在Horn集上完备。集上完备。.处理等词的方法处理等词的方法l调解调解(1969,Wos)1993，1994，欧阳丹彤，孙吉贵，刘叙华。输入归结与，欧阳丹彤，孙吉贵，刘叙华。输入归结与输入对称调解对输入对称调解对Horn集完备；单元归结与对称调解对集完备；单元归结与对称调解对Horn集完备（集完备（1990）；软件学报及英文版）；软件学报及英文版1992，欧阳丹彤，刘叙华，输入归结与输入有向调解对，欧阳丹彤，刘叙华，输入归结与输入有向调解对Horn集不完备；一定条件下完备；吉林大学学报集不完备；一定条件下完备；吉林大学学报lRUE(1986,Digricoli)1987,欧
82、阳继红，欧阳继红，RUE对于带等词的基子句集完备的；单对于带等词的基子句集完备的；单元及输入元及输入RUE在在Horn集上完备；锁集上完备；锁RUE完备。完备。1994，欧阳丹彤，刘叙华，欧阳丹彤，刘叙华，Strong形形RUENRF归结不归结不完备。完备。计算机学报计算机学报.七、广义归结七、广义归结1979,王湘浩，刘叙华王湘浩，刘叙华定定义义（广广义义子子句句）设设A1, , An是是一一些些原原子子, (A1, , An)是以是以逻辑联结词逻辑联结词、联结这联结这些原子和一些些原子和一些0，1做成的公式做成的公式,称称为为广广义义子句子句,其其中中 0代表代表F，1代表代表T。常子句：
83、常子句：没有原子出没有原子出现现，只有，只有0或者或者1的广的广义义子句。子句。零子句：零子句：其其值为值为0的常子句。的常子句。壹子句：壹子句：其其值为值为1的常子句。的常子句。定定义义（广广义义子句的因子子句的因子） 设设 (A1, , An)是一个广是一个广义义子子 句，句，Ai1, , Air有一个有一个mgu （1 ij n, j=1, , r），）， 则则称称 为为 的因子。的因子。.定定义义（广（广义归结义归结式）式）设设 , 是无公共是无公共变变元的广元的广义义子句子句, 是合一是合一Ai1, , Air所得的因子，所得的因子， 是合一是合一Bj1, , Bjs所得的因子。所得
84、的因子。 设设 是是Ai1 和和Bj1 的的mgu，于是，于是， (Ai1=0) (Bj1=1) (Ai1=1) (Bj1=0)都称都称为为 与与 的广的广义归结义归结式。式。.l例例.设设S是如下一个广义子句集：是如下一个广义子句集：(1)PQ(2)P(3)Q从从S推出零子句的一个广义归结演绎如下：推出零子句的一个广义归结演绎如下：(4)(1Q) 0(1)、(2)(5)(10) 0 (1)=0(3)、(4).l广义归结在广义子句集上完备。广义归结在广义子句集上完备。l广义锁、广义线性、广义语义归结加一定条件广义锁、广义线性、广义语义归结加一定条件完备。完备。l1995，刘叙华，欧阳丹彤，广义，刘叙华，欧阳丹彤，广义Horn集；广集；广义义Horn集上广义输入归结与广义输入对称调集上广义输入归结与广义输入对称调解完备；一定条件下，广义解完备；一定条件下，广义Horn集上广义输集上广义输入归结与广义输入有向调解完备；入归结与广义输入有向调解完备；软件学软件学报报.
