戏定义7、设0={t1/x1,t2/x2…tn/xn}是一个替 换,E是一个表达式(项、原子公式、文字、 子句),把E中出现的所有个体变元x都用t1替 换,得到的结果记为Eθ,称为E在0下的替换 实例。 例、若E=P(xyg(z),0={a/x,f(b)/y,c/z},则 E0= P(a, f(b),gc))
定义７、设＝{t1 / x1 , t2 / x2 ,…,tn / xn }是一个替 换，E是一个表达式（项、原子公式、文字、 子句），把E中出现的所有个体变元xi都用t i 替 换，得到的结果记为E ，称为E在下的替换 实例。 例、若E=P(x,y,g(z)), ＝{a / x, f(b) /y ,c /z }，则 E= P(a,f(b),g(c))
定义8、设0={t1/x,t2/x2,…,tn/xn},= {u1/y,2/y2,…,um/ymn}是两个替换,则将集合 m}中符合下列条的两种情形删除: 1)、t12/x2,当14=x1。 2)、l1/y,当y∈{x1 得到的集合仍是一个替换,称为0与λ的复合,记为 0° 例、见教材p67例3.13
定义８、设＝{t1 / x1 , t2 / x2 ,…,tn / xn }， ＝ {u1 / y1 , u2 / y2 ,…,um / ym }是两个替换，则将集合 {t1 / x1 , t2 / x2 ,…,tn / xn，u1 / y1 , u2 / y2 ,…,um / ym }中符合下列条件的两种情形删除： １）、 t i / xi ，当t i ＝ xi 。 ２）、 ui / yi ，当yi { x1 , x2 ,…, xn } 。 得到的集合仍是一个替换，称为与的复合，记为 º。 例、见教材p67例3.13
定义9、设S={F1,F2,Fn}是一个原子谓词公式集, 若存在一个替换θ,使得F10=F20=…=Fn0,则 称0为S的一个合一( Unifier),并称S为可合一的。 一个公式集的合一一般不唯一。 定义10、设σ是公式集S的一个合一,如果对S的任 何一个合一0,都存在一个替换λ,使得θ=σ°, 则称σ为S的一个最一般合一( Most general Unifier),简称MGU
定义９、设S= { F1 , F2 ,…, Fn }是一个原子谓词公式集， 若存在一个替换，使得F1 ＝F2 ＝…＝Fn ，则 称为S的一个合一（Unifier），并称S为可合一的。 一个公式集的合一一般不唯一。 定义１０、设是公式集S的一个合一，如果对S的任 何一个合一，都存在一个替换，使得＝ º， 则称为S的一个最一般合一（Most General Unifier），简称MGU
定义11、设S是一个非空的具有相同谓词名 的原子公式集,从S中各公式的左边第一个 项开始,同时向右比较,每一组不都相同的 项的差异部分组成的集合称为S的差异集。 例、公式集S={P(a,xf(g(y)),P(zh(z,u),f(u)}的 差异集为{a,z},{xh(zu)},{gy)u}
定义１１、设S是一个非空的具有相同谓词名 的原子公式集，从S中各公式的左边第一个 项开始，同时向右比较，每一组不都相同的 项的差异部分组成的集合称为S的差异集。 例、公式集S={P(a,x,f(g(y))),P(z,h(z,u),f(u))}的 差异集为{a,z}, {x,h(z,u)}, {g(y),u}
3.23替换与合 设S为一非空有限具有相同谓词名的原子谓词 公式集,求S的MGU的算法: (1)、令k=0,Sk=S,σ=E(E表示空替换) (2)、若S只含有一个谓词公式,则算法停止,σk 就是要求的最一般合 (3)、求S的差异集D。 (4)、若D中存在元素x和t,其中ⅹ是变元,t 是项且x不在t中出现,则置Sk+1=Sk{t/x},σk+1 =G°{tx},k=k+1,然后转步(2)。 (5)、算法停止,S的最一般合一不存在
3.2.3 替换与合一 设S为一非空有限具有相同谓词名的原子谓词 公式集，求S的MGU的算法： （1）、令k=0, Sk=S, k= （ 表示空替换）。 （2）、若Sk只含有一个谓词公式，则算法停止， k 就是要求的最一般合一。 （3）、求Sk的差异集Dk 。 （4）、若Dk中存在元素 xk 和 tk ，其中xk是变元， tk 是项且xk不在tk中出现，则置Sk+1 = Sk{tk /xk} ， k+1 = k º{tk /xk} ，k=k+1，然后转步（2）。 （5）、算法停止，S的最一般合一不存在