吉林大学研究生人工智能t演示文档

《吉林大学研究生人工智能t演示文档》由会员分享，可在线阅读，更多相关《吉林大学研究生人工智能t演示文档（127页珍藏版）》请在装配图网上搜索。

.,6/27/2018,1,第六章 归结原理,6.1 子句集的Herbrand域 一、 Herbrand域与 Herbrand解释 定义（Herbrand域）设S为子句集，令H0是出现于子句集S的常量符号集。如果S中无常量符号出现，则H0由一个常量符号a组成。 对于i＝1，2，…，令 Hi = Hi-1｛所有形如f(t1，…，tn)的项｝ 其中f(t1，…，tn)是出现在S中的所有n元函数符号， tj Hi-1，j＝1，…，n． 称Hi为S的i级常量集，H 称为S的Herbrand域， 简称S的H域。,.,6/27/2018,2,,例 S＝｛P(f(x)，a，g(y)，b)｝ H0 ={a, b} H1 ={a, b, f(a), f(b), g(a), g(b)} H2＝{a, 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))} …,.,6/27/2018,3,练习: 求S的Herbrand域,S＝{P(x)  Q(y)，R(z) } S＝{Q(a) ～P(f(x))， ～Q(b)  P(g(x,y)) },.,6/27/2018,4,原子集 基例,基：把对象中的变量用常量代替后得到的无变量符号出现的对象。 基项、基项集、基原子、基原子集合、基文字、基子句、基子句集 定义 (原子集、Herbrand底) 设S是子句集，形如P(t1,…,tn)的基原子集合，称为S的Herbrand底或S的原子集． 其中P(x1，…，xn)是出现于S的所有n元谓词符号，t1，…，tn是S的H域中的元素． 定义（基例） 设S是子句集，C是S中的一个子句．用S的H域中元素代替C中所有变量所得到的基子句称为子句C的基例。,.,6/27/2018,5,练习,已知S＝｛P(f(x)，a，g(y)，b)｝，求S的原子集， 给出P(f(x)，a，g(y)，b)的一个基例。 已知S＝{P(x)  Q(y)，R(z) }，求S的原子集， 分别给出P(x)  Q(y)， R(z)的所有基例。 已知S＝ {Q(a)～P(f(x))，～Q(b) P(g(x,y))}， 求S的原子集， 分别给出Q(a)～P(f(x)) ， ～Q(b) P(g(x,y))的一个基例。 设S＝{P(x), Q(f(y))  R(y) }，求S的H域， S的原子集， P(x)的基例, Q(f(y))  R(y) 的基例。,.,6/27/2018,6,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的原子集。于是S的一个H解释I可方便地表示为如下一个集合： I* ＝｛m1，m2，…，mn，…｝ 其中, mi =,,,.,6/27/2018,7,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)), … },.,6/27/2018,8,练习,S={P(x)Q(x), ～P(a), ～Q(b) }， 求S的所有H解释。,.,6/27/2018,9,二、Herbrand解释与普通解释的关系,子句集S的H解释是S的普通解释。 S的普通解释不一定是S的H解释：普通解释不是必须定义在H域上，即使定义在H域上，也不一定是一个H解释。 任取普通解释I，依照I，可以按如下方法构造S的一个H解释I*，使得若 S在 I下为真则 S在I*下也为真。,.,6/27/2018,10,例.,S＝｛P(x), Q(y,f(y,a))｝ 令S的一个解释I如下： D＝{1，2} a f(1, 1) f(1, 2) f(2, 1) 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)), …｝,.,6/27/2018,11,例,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) 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)), …｝,.,6/27/2018,12,对应于I的H解释I*,定义（对应于I的H解释I*） 设I是子句集S在区域D上的解释。H是S的H域。  是如下递归定义的H到D的映射： 1） ①若S中有常量符号,H0是出现在S中所有常量符号的集合。 对任意aH0，规定 (a)=I(a)． ②若S中无常量符号,H0={a}。 规定 (a)=d,d∈D。 2）对任意(h1,…,hn)Hin,及S中任意n元函数符号f(x1,…,xn) , 规定(f(h1，…，hn)) =I(f(h1，…，hn)) 。,.,6/27/2018,13,对应于I的H解释I*,对应于I的H解释I*是如下的一个H解释： 任取S中n元谓词符号P(x1,…,xn)， 任取(h1,…,hn)Hn，规定 TI*(P(h1，…，hn))=TI(P(h1，…，hn)),.,6/27/2018,14,引理 如果某区域D上的解释I满足子句集S， 则对应于I的任意一个H解释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,,.,6/27/2018,15,,因为对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）Dn。 i=1, … ,m。 故对任意（h1，…，hn）Hn ，都有 TI*(Ci（h1，…，hn）)=T, 故TI*(S)=T，即I*满足S。,.,6/27/2018,16,,只考虑子句集的H解释是否够用？ 定理 子句集S恒假当且仅当S被其所有H解释弄假。 证明: 必要性显然。 充分性。假设S被其所有H解释弄假，而S又是可满足的。 设解释I满足S，于是由引理知，对应于I的H解释I*也满足 S，矛盾．故S是不可满足的． 从现在起，如不特别指出，提到的解释都是指H解释．,.,6/27/2018,17,结论,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)),.,6/27/2018,18,,2）子句C被解释I满足，当且仅当 C的每一个基例都被I满足． 3）子句 C被解释 I弄假，当且仅当 至少有一个C的基例C’被I弄假。,.,6/27/2018,19,例.,C=～P(x)Q(f(x)) I1={～P(a),～Q(a),～P(f(a)),～Q(f(a)),～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。,.,6/27/2018,20,,4）子句集S不可满足，当且仅当 对每个解释I，至少有一个S中某个子句C的基例C’被I弄假。,.,6/27/2018,21,6.2 Herbrand定理,Herbrand定理是符号逻辑中一个很重要的定理．Herbrand定理就是使用语义树的方法，把需要考虑无穷个H解释的问题，变成只考虑有限个解释的问题．,.,6/27/2018,22,一、语义树,定义(互补对) 设 A是原子，两个文字A和～A都是另一个的补，集合｛A，～A｝称为一个互补对． 定义(Tautology,重言式) 含有互补对的子句．,.,6/27/2018,23,定义 （语义树） 设S是子句集，A是S的原子集．关于S的语义树是一棵向下生长的树T．在树的每一节上都以如下方式附着A中有限个原子或原子的否定： 1）对于树中每一个节点N，只能向下引出有限的直接的节 L1，…，Ln． 设Qi是附着在Li上所有文字的合取，i=1, … ,n， 则Q1…Qn是一个恒真的命题公式． 2）对树中每一个节点 N，设 I（N）是树T由根向下到节点 N 的所有节上附着文字的并集， 则I（N）不含任何互补对．,语义树,.,6/27/2018,24,完全语义树,定义（完全语义树） 设A={A1,…,An,…｝是子句集S的原子集． S的一个语义树是完全的，当且仅当 对于语义树中每一个尖端节点N（即从N不再 生出节的那种节点），都有 Ai或～Ai有且仅有一个属于I(N),i=1,…,k,…,.,6/27/2018,25,,例. 设A=｛P，Q，R｝是子句集S的原子集， 完全语义树(正规完全语义树 ),.,6/27/2018,26,,,.,6/27/2018,27,例. 设 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))), …},,.,6/27/2018,28,语义树与解释,S的完全语义树的每一个分枝都对应着S的一个解释； 定义（部分解释）对于子句集S的语义树中的每一个节点N,I(N)是S的某个解释的子集，称I(N)为S的部分解释。 S的任意解释都对应着S的完全语义树中的一条分枝？ 综合： 子句集S的一棵完全语义树对应着S的所有解释。,.,6/27/2018,29,证明: 若不然，设T中节点N向下生出的n个节L1，…，Ln的每个节Li上，都至少有一个文字Ai不在I中． 由语义树的定义知：Q1…Qn是恒真公式,其中Qi表示Li 上所有文字的合取，i=1, …, n。将Q1…Qn化为合取范式： Q1…Qn＝（A1A2…An）(…) … (…) 因为每一个析取式中都必须有一个互补对。不妨设 A1＝～A2,于是A2,～A2都不在I中,这与I是一个解释矛盾。 结论：对S的任意解释I，都可以从S的完全语义树的根点出发，向下找出一条分枝，使该分枝对应着解释I。,引理 设T是子句集S的完全语义树，I是S的一个解释。于是T中任意节点向下生出的直接节中，必有一节，其上所有文字都在I中。,.,6/27/2018,30,子句集的封闭语义树,定义（失效点） 称语义树T中的节点N为失效点，如果 (1)I(N)弄假S中某个子句的某个基例； (2)I(N’)不弄假S中任意子句的任意基例，其中N’是 N的任意祖先节点。 定义（封闭语义树） 语义树T是封闭的，当且仅当T的每—个分枝的终点都是失效点。 定义（推理点）称封闭语义树的节点 N为推理点，如果N的所有直接下降节点都是失效点．,.,6/27/2018,31,例. 设S={P, ～PR, ～P～Q, ～P～R}。,S的原子集 A={P, Q, R},,,,,,,,,,,,,,,,P,~P,Q,~Q,Q,~Q,R,~R,R,~R,R,~R,R,~R,.,6/27/2018,32,练习,设子句集 S={～P(x)∨Q(x),P(f(x)), ～Q(f(x))} 分别画出S的完全语义树与 封闭语义树。,.,6/27/2018,33,二、Herbrand定理,Herbrand定理I．子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义树． 证明: 必要性： 若S是不可满足的，设T是S的完全语义树． 对T的每一个分枝B,令IB是附着在B上所有文字的集合， 则IB是S的一个解释,故IB弄假S中某子句C的某个基例C’． 由于C’是有限的，所以B上存在一个节点NB使得部分解 释I（NB）弄假C’，于是分枝B上存在失效点． 因此，对T中每一分枝都存在一个失效点，于是从T得到 S的一个封闭语义树T’。,.,6/27/2018,34,Herbrand定理I．子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义树．,(有限性) 因为封闭语义树T’中每一个节点只能向下生长有限个节,故T’必有有限个节点.否则,由Konig无限性引理,T’中必有一条无穷的分枝,此无穷分枝上当然没有失效点,矛盾。 （Konig无限性引理：在一个其点之次数有限的无限有向树中，必有一源于根的无限路。 ） 充分性： 若S的每一个完全语义树T都对应着一个有限封闭语义树 T’，则T的每条分枝上都有一个失效点。因为S的任一解 释都对应T的某一条分枝，所以每一个解释都弄假S， 故S是不可满足的。,.,6/27/2018,35,Herbrand定理II 子句集S是不可满足的，当且仅当存在S的一个有限不可满足的S的基例集S’。,证明: 必要性： 若S恒假，设T是S的完全语义树，由 Herbrand定理I知，有一个有限封闭 语义树 T’对应着T。 令S’是被 T’中所有失效点弄假的所有 基例（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), P(b), ～P(a)∨～P(b)},.,6/27/2018,36,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是不可满足的。,.,6/27/2018,37,,Herbrand定理II提出了一种证明子句集S的不可满足性的方法：如果存在这样一个机械程序，它可以逐次生成S中子句的基例集 S0’，…，Sn’，并逐次地检查S0’，…，Sn’，…的不可满足性，那么根据 Herbrand定理，如果 S是不可满足的，则这个程序一定可以找到一个有限数N，使SN’是不可满足的。,.,6/27/2018,38,使用Herbrand定理的机器证明过程,Gilmore过程 D-P过程,.,6/27/2018,39,Gilmore过程（1960年）,逐次地生成S0’， S1’…，Sn’，…，其中Si’是用S的i级常量集合Hi中的常量，代替S中子句的变量，而得到的S的所有基例之集合。 对于每一个Si’，可以使用命题逻辑中的任意的方法去检查Si’的不可满足性。 Gilmore使用了所谓乘法方法：即将Si’化为析取范式。如果其中任意一个合取项包含一个互补对，则可以删除这个合取项，最后，如果某个Si’是空的，则Si’是不可满足的。 当S不可满足时，该算法一定结束(半可判定)。,.,6/27/2018,40,,例. S={P(a), ～P(x) Q(f(x)), ～Q(f(a)) } H0={a} S0=P(a) (～P(a) Q(f(a))) ～Q(f(a)) =(P(a)～P(a)～Q(f(a)))(P(a) Q(f(a)))～Q(f(a))) = = 所以，S是不可满足的。 该算法具有指数复杂性，为此提出了改进规则，称为Davis-Putnam预处理----检验基子句集不可满足性。,.,6/27/2018,41,D-P过程,设S是基子句集 Tautology删除规则 设S’为删去S中所有的Tautology所剩子句集， 则 S恒假 iff S’恒假。,.,6/27/2018,42,,单文字规则 若S中有一个单元基子句L， 令S’为删除S中包含L的所有基子句所剩子句集， 则： (1) 若S’为空集，则S可满足。 (2) 否则， 令S’’为删除S’中所有文字～L所得子句集 （若S’ 中有单元基子句～L，则删文字～L 得空子句）， 于是， S恒假 iff S’’恒假。 S=L∧(L∨C1’) ∧… ∧(L∨Ci’) ∧ (～L∨Ci+1’) ∧… ∧ (～L∨Cj’) ∧ Cj+1 ∧… ∧ Cn,.,6/27/2018,43,,定义（纯文字）：称S的基子句中文字L是纯的，如果～L不出现在S中。 纯文字规则 设L是S中纯文字，且S’为删除S中所有包含L的基子句所 剩子句集，则 (1)若S’为空集，则S可满足。 (2) 否则，S恒假 iff S’恒假。 S=(L∨C1’) ∧… ∧(L∨Ci’) ∧ Ci+1 ∧… ∧ Cn,.,6/27/2018,44,,分裂规则 若S=(A1 L) …  (Am L)  (B1  ～L)  …  (Bn  ～L) R 其中A i , Bi ,R都不含L或～L，令 S1 =A1 …  Am R S2= B1  …  Bn R 则S恒假 iff S1 ， S2同时恒假。,.,6/27/2018,45,Davis-Putnam方法练习,S= (PQ～R) (P～Q) ～P R U S= (P～Q) (～PQ)  (Q～R)  (～Q～R) S= (PQ) (P～Q)  (RQ)  (R～Q),.,6/27/2018,46,Herbrand定理的主要障碍,要求生成关于子句集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=1512个元素} S5’是不可满足的，但是H5’是1065数量级个元素，而S5’有10260数量级的元素。想将S5’存储起来都是不可能的，更不要说是检查它的不可满足性了。,.,6/27/2018,47,为了避免像Herbrand定理所要求的那样去生成子句的基例集，J.A.Robinson于1965年提出了归结原理，归结原理可以直接应用到任意子句集S上（不一定是基子句集），去检查S的不可满足性。 归结原理的本质思想是去检查子句集S是否包含一个空子句: 如果S包含，则S是不可满足的。 如果S不包含，则去检查是否可由S推导出来。 当然这个推理规则必须保证推出的子句是原亲本子句的逻辑结果。归结原理就是具有这种性质的一种推理规则。,归结原理思想,.,6/27/2018,48,命题逻辑中的归结原理,,.,6/27/2018,49,归结式,定义（归结式） 对任意两个基子句C1和C2。如果C1中存在文字L1，C2中存在文字L2，且L1＝～L2， 则从C1和C2中分别删除L1和L2，将C1和C2的剩余部分析取起来构成的子句，称为C1和C2的归结式，记为R(C1, C2)。 C1和C2称为亲本子句。,.,6/27/2018,50,练习:求下述各子句对的归结式,C1= ～PQR, C2=～QS C1= PQ～R, C2=～P RQ,.,6/27/2018,51,定理 设C1和C2是两个基子句， R(C1, C2) 是C1，C2的归结式，则R(C1, C2)是C1和C2的逻辑结果。 证明： 设 C1=L C1’, C2=～LC2’。于是 R(C1, C2) ＝C1’ C2’ 设I是C1和C2的一个解释，且满足C1也满足C2。因为L和～L中有一个在I下为假，不妨设为L。于是C1’非空，且在I下为真。故R(C1, C2)在I下为真。,命题逻辑归结方法的可靠性,.,6/27/2018,52,归结演绎,定义（归结演绎） 设S是子句集。从S推出子句C的一个归结演绎是如下一个有限子句序列： C1，C2，…，Ck 其中Ci或者是S中子句，或者是Cj和Cr的归结式 (ji, r i)； 并且Ck＝C。 称从子句集S演绎出子句C，是指存在一个从S推出C的演绎。 定理 若从子句集S可以演绎出子句C，则C是S的逻辑结果。 推论 若子句集S是可满足的， 则S推出的任意子句也是可满足的。,.,6/27/2018,53,,定义 从S推出空子句的演绎称为一个反驳（反证） ，或称为S的一个证明。 结论：若从基子句集S可演绎出空子句，则S是不可满足的。 演绎树：从子句集S出发，通过归结原理可得到一个向下的演绎树，其每个初始节点上附着一个S中子句，每个非初始节点上附着一个其前任节点上子句的归结式。,.,6/27/2018,54,例. S={PQ, ～PQ, P～Q, ～P～Q },归结演绎： (1) PQ (2) ～PQ (3) P～Q (4) ～P～Q (5) Q 由(1)、(2) (6) ～Q 由(3)、(4) (7)  由(5)、(6),.,6/27/2018,55,归结原理一般过程:,1)建立子句集S。 2)如果S含空子句，则结束。 3)从子句集S出发,仅对S的子句间使用归结推理规则。 4)如果得出空子句，则结束。 5)将所得归结式仍放入S中。 6)对新的子句集使用归结推理规则。转4)。,.,6/27/2018,56,例.证明(P Q) ~Q  ~p,首先建立子句集: S={~PQ, ~Q , P} 归结演绎: (1) ~P Q (2) ~ Q (3) P (4) ~P (1)(2)归结 (5)  (3)(4)归结,.,6/27/2018,57,命题逻辑归结原理的完备性,定理 如果基子句集S是不可满足的， 则存在从S推出空子句的归结演绎。 证明： 设M是S的原子集，对M的元素数|M|用归纳法。 当|M|=1时，设原子为P。 若∈S ，得证。 否则，因为S是不可满足的，于是，S中必包含单元子 句P和～P，而P和～P的归结式是，所以存在从S推出的 归结演绎。 假设|M|n (n≥2) 时，定理成立。往证 |M|＝n时定理成立。,.,6/27/2018,58,,取M中任意一原子P，做如下两个子句集： S’：将S中所有含P的子句删除，然后在剩下的子 句中删除文字～P； S”：将S中所有含～P的子句删除，然后在剩下的 子句中删除文字P。 显然，S’和S”都不可满足，且它们的原子集的元 素数都小于n。根据归纳假设，存在从S’推出  的 归结演绎D1，从S”推出的归结演绎D2。,.,6/27/2018,59,,S={P∨C1’, … ,P∨Ci’ , ～P∨Ci+1’,… ,～P∨Cj’, Cj+1 ,… , Cn} S’={Ci+1’,… ,Cj’,Cj+1 ,… , Cn} S’’={C1’, … ,Ci’ , Cj+1 ,… , Cn} 例： S={PQ, P～Q, ～PR, ～ R} M={P,Q,R},.,6/27/2018,60,,在D1中，将S’中所有不是S中的子句，通过 添加文字～P而恢复成S中子句，于是，得到从S 推出  或者～P的归结演绎D1’。 用同样方法从D2可得一个从S推出  或者P的 归结演绎D2’。 显然，从D1’和D2’就不难得到一个从S推出  的 归结演绎D。 归纳法完成。,.,6/27/2018,61,,Resolution Principle 两种译法： 归结原理：从内部看 刘叙华，一种新的语义归结原理，吉林大学学报，1978。 消解原理：从外部看 马希文，机器证明及其应用，计算机应用， 1978。,.,6/27/2018,62,6.3 合一算法,,.,6/27/2018,63,,例1 C1：P(x)  Q(y) C2：~P(a)  R(z) 例2 C1：P(x)  Q(x) C2：~P(f(x))  R(x) 替换和合一是为了处理谓词逻辑中子句之间的模式匹配而引进.,.,6/27/2018,64,一、替换与最一般合一替换,定义(替换)一个替换是形如{t1/v1, … , tn/vn }的一个有限集合，其中vi是变量符号，ti是不同于vi的项。并且在此集合中没有在斜线符号后面有相同变量符号的两个元素，称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是基项时，称此替换为基替换。 空替换：没有元素的替换称为空替换，记为。,.,6/27/2018,65,替换,定义（改名） 设替换  ={ t1/x1, … , tn/xn } 如果t1, … , tn是不同的变量符号，则称为一个改 名替换，简称改名。 替换作用对象：表达式（项、项集、原子、原子集、 文字、子句、子句集） 基表达式：没有变量符号的表达式。 子表达式：出现在表达式E中的表达式称为E的子 表达式。,.,6/27/2018,66,E的例,定义（E的例） 设  ={ t1/v1, … , tn/vn }是一个替换，E是一个表达式。将E中出现的每一个变量符号，vi (1 i n) ，都用项ti替换，这样得到的表达式记为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),,.,6/27/2018,67,,练习： E=P(x, g(y), h(x,z)), ={a/x, f(b)/y, g(w)/z} E=P(a, g(f(b)), h(a,g(w))) E=P(x, y, z), ={y/x, z/y} E=P(y, z, z). EP(z, z, z).,.,6/27/2018,68,替换的乘积,定义（替换的乘积）设 ={ t1/x1, … , tn/xn }， ={ u1/y1, … , um/ym} 是两个替换。将下面集合 { t1/x1, … , tn/xn , u1/y1, … , um/ym } 中任意符合下面条件的元素删除： 1）ui/yi，当yi{x1, … , xn }时； 2）ti/xi，当ti = xi 时。 如此得到一个替换，称为与的乘积，记为 。 例. 令  ={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, y/z }  与的乘积为   = {f(b)/x, y/z },.,6/27/2018,69,,={a/x}, ={b/x} ={a/x} ={b/x} 可见：  ,.,6/27/2018,70,,例子: E=P(x, y, z) ={a/x, f(z)/y, w/z} E=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)/w} E=P(a, f(t), g(b)),.,6/27/2018,71,引理 若E是表达式，，是两个替换， 则E ( ) = (E),证明： 设vi是E中任意一个变量符号，而  ={ t1/x1, … , tn/xn }，  ={ u1/y1, … , um/ym } 若vi既不在{ x1, … , xn }中，也不在{ y1, … , ym }中，则vi在E ( )中和在(E)中都不变。 若vi=xj (1jn)，则E中的vi，在(E)中先变成tj，然后再变成tj；E中的vi在E()中立即就变成了tj。故E中vi在(E)中和在E()中有相同变化。 若vi=yj (1jm)，且yj{ x1,…,xn }，则E中vi在(E)中变为uj;E中vi在E()中也变为uj(注意:yj{x1,…, xn}，所以uj/yj），故E中vi在(E)中和在E ()中有相同变化。 由于vi的任意性，故引理得证。,.,6/27/2018,72,引理 设，， 是三个替换， 于是()＝(),证明： 设E是任一表达式，由上面引理知 E(()) =(E()) = ((E)) E(()) =(E) () = ((E)) 所以 E(()) = E(()) 由于E的任意性，故 ()＝(),.,6/27/2018,73,,定义(合一)称替换是表达式集合{E1,…,Ek}的 合一，当且仅当E1＝E2=…=Ek。 表达式集合｛E1, … , Ek｝称为可合一的，如果存在关于此集合的一个合一。 定义(最一般合一) 表达式集合｛E1, … , Ek｝的合一 称为是最一般合一(most general unifier, 简写为mgu)，当且仅当对此集合的每一个合一，都存在替换，使得 ＝,.,6/27/2018,74,,例. 表达式集合｛P(a, y), P(x, f(b))｝是可合一的，其最一般合一＝{a/x, f(b)/y}。显然，这也是此集合的mgu。 ？ 表达式集合｛P(a, b), P(x, f(b))｝是否可合一？ 例. 表达式集合｛P(x), P(f(y))｝是可合一的，其最一般合一＝{f(y)/x} ＝{f(a)/x, a/y}也是合一，有替换 ={a/y}，使 ＝={f(y)/x}{a/y},.,6/27/2018,75,,例 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},.,6/27/2018,76,二、合一算法,定义（差异集合） 设W是非空表达式集合，W的差异集合是如下一个集合：首先找出W的所有表达式中不是都相同的第一个符号，然后从W的每一个表达式中抽出占有这个符号位置的子表达式。所有这些子表达式组成的集合称为这步找到的W的差异集合D。,.,6/27/2018,77,W不可合一的三种情况,（1）若D中无变量符号为元素，则W是不可合一的。 例. W={P(f(x)), P(g(x))} D={f(x), g(x)} （2）若D中有奇异元素和非奇异元素，则W是不可合一的。 例. W={P(x), P(x, y)} D={⊙, y} （3）若D中元素有变量符号x和项t，且x出现在t中，则W是不可合一的。 例. W={P(x), P(f(x))} D={x, f(x)},.,6/27/2018,78,,换名: {P(f(x), x), P(x, a)}; 如果不换名：D={f(x), x}. 换名: {P(f(y), y), P(x, a)}; mgu: {f(a)/x, a/y},.,6/27/2018,79,步骤1：置 k=0, Wk=W, k= 步骤2：若Wk只有一个元素，则停止，k是W的最一般合一； 否则，找出Wk的差异集合Dk。 步骤3：若Dk非奇异，Dk中存在元素vk和tk，其中vk是变量符号，并且 不出现在tk中，则转步骤4； 否则，算法停止，W是不可合一的。 步骤4：令 k+1=k{tk/vk}，Wk+1=Wk （注：Wk+1=W ） 步骤5：置 k=k+1，转步骤2。,合一算法（Unification algorithm）,,,.,6/27/2018,80,例. 令 W={Q(f(a), g(x)), Q(y, y)}, 求W的mgu。,步骤1： k=0, W0=W, 0=。 步骤2： D0 ={f(a), y}。 步骤3：有v0= y D0，v0不出现在t0＝f(a)中。 步骤4：令 1=0{t0/v0}={f(a)/y}, W1={Q(f(a), g(x)), Q(f(a), f(a))} 步骤5：k=k+1=1 步骤2： D1 ={g(x), f(a) }。 步骤3：D1中无变量符号，算法停止，W不可合一。 ？ 若令W={Q(f(a), g(x)), Q(y, z)}, W是否可合一？,.,6/27/2018,81,例 令 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= z D0，v0不出现在t0＝a中。 步骤4：令 1=0{t0/v0}={a/z}={a/z}， W1=W0{t0/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= x D1，且v1不出现在t1＝f(a)中。 步骤4：令 2=1{t1/v1}={a/z} { f(a)/x }={a/z, f(a)/x }， W2=W1{t1/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))},.,6/27/2018,82,例.,步骤5：k=k+1=2 步骤2： D2 ={g(y), u}。 步骤3：有v2= u D2，且v2不出现在t2＝g(y)中。 步骤4：令 3=2{t2/v2}={a/z, f(a)/x } { g(y)/u } ={a/z, f(a)/x, g(y)/u }， W3=W2{t2/v2}={P(a, f(a), f(g(y))), P(a, f(a), f(u))}{ g(y)/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的最一般合一。,.,6/27/2018,83,定理 若W是关于表达式的有限非空可合一集合，则合一算法终将结束在步骤2，并且最后的k是W的最一般合一。,证明： （1）终止性。 否则将产生一个无穷序列： W ， W ，…， W ，… 其中每一个直接后继集合比它的前任都少一个变量符号（注意：W 包含vk，而W 不包含vk）。但这是不可能的，因为W仅含有限个变量符号。 （2） k是W的合一。若算法停止在步骤2，则Wk=W只含有一个元素，所以k是W的合一。,,,,,,.,6/27/2018,84,,（3）用归纳法证明算法必不会停止在步骤3，并且对任意W的一个合一，任意k，都存在替换k，使得 =kk 亦即k是W的mgu。 当k=0时，因0=，取0=，于是==00。,.,6/27/2018,85,假设对0kn，=kk成立。 往证：存在n+1，使得=n+1n+1。 若W 只含有一个元素，则合一算法结束在步骤2。因为=nn，且n是W的合一，故n是W的mgu。定理得证。 若W 不只含有一个元素,按照算法,将找出W的差异集合Dn。 因为=nn是W的合一，所以W中表达式经替换作用后都变成同一个相同的表达式。而W中表达式经n作用后，产生了差异集合Dn，所以Dn必须被n所统一，即n是D n的合一。,.,6/27/2018,86,,因为Dn是可合一的（n就是Dn的合一），所以必有变量符号vnDn；Dn中至少有两个不同元素。所以可设tnDn，且tn≠vn。显然，变量符号vn不出现在tn中（否则，vnn≠ tnn，这与n是Dn的合一矛盾）。 因此算法不能停止在步骤3，所以算法必然停止在步骤2。,.,6/27/2018,87,,令n+1=n{tn/vn}。因为vnn=tnn,所以tnn/vnn 令n+1=n -{tnn/vn}。因vn不出现在tn中，所以 于是 故 归纳法完成。即对所有k≥0,都存在替换k，使=kk。所以算法终止步骤2时，k是W的最一般合一。,,,,.,6/27/2018,88,6.4 一阶逻辑中的归结原理,,.,6/27/2018,89,,定义（因子） 如果子句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的因子。,.,6/27/2018,90,二元归结式,定义 设C1, C2是两个无公共变量的子句(称为亲本子句), L1, L2分别是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。取L1＝P(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的二元归结式.,.,6/27/2018,91,,练习：设C1=P(a) R(x), C2=～P(y) Q(b) 求C1和C2的二元归结式.,.,6/27/2018,92,,在谓词逻辑中，对子句进行归结推理时，要注意 的几个问题： （1）若被归结的子句C1 和C2中具有相同的变元时，需要将其中一个子句的变元更名，否则可能无法合一，从而没有办法进行归结。,.,6/27/2018,93,,例： C1=P(x), C2=～P(f(x)) 例：设知识库中有如下知识： (1)若x的父亲是y，则x不是女人。 (2)若x的母亲是y，则x是女人。 (3)Chris的母亲是Mary。 (4)Chris的父亲是Bill。 求证：这些断言包含有矛盾。 father(x,y):x的父亲是y mother(x,y):x的母亲是y woman(x):x是女人,.,6/27/2018,94,,（2）在求归结式时,不能同时消去两个互补文字对,消去两个互补文字对所得的结果不是两个亲本子句的逻辑推论。 例.设C1=P(x) ～Q(b), C2=～P(a) Q(y)R(z) 求C1和C2的二元归结式. （3）如果在参加归结的子句内含有可合一的文字,则在进行归结之前,应对这些文字进行合一,以实现这些子句内部的化简。,.,6/27/2018,95,归结式,定义 子句C1, C2的一个归结式是下列二元归结式之一： C1和C2的二元归结式。 C1和C2的因子的二元归结式。 C1的因子和C2的二元归结式。 C1的因子和C2的因子的二元归结式。 例. 设 C1=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),.,6/27/2018,96,一阶逻辑归结原理的完备性,提升引理 如果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)),.,6/27/2018,97,一阶逻辑归结原理的完备性,定理 若子句集S是不可满足的，则存在从S推出空子句的归结演绎。 证明: 设子句集S是不可满足的，由Herbrand定理II知，存在S的一个基例集S’也是不可满足的。 根据命题逻辑归结原理的完备性，存在从S’推出空子句的归结演绎D’。 由提升引理知，可将D’提升成一个从S推出空子句的归结演绎D。定理得证。,.,6/27/2018,98,,应用归结原理的习题,.,6/27/2018,99,6.5 归结原理的几种改进,,.,6/27/2018,100,,水平浸透法（Level Saturation Method） S0= S Sn= {C1和C2的归结式| C1∈S0∪…∪Sn-1，C2 ∈Sn-1},.,6/27/2018,101,例.使用水平浸透法证明 S={P∨Q,～P∨Q, P∨～Q, ～P∨～Q} 不可满足。,