公式集的合一

大家好，欢迎来到IT知识分享网。

定义3.3 设有公式集F={F1,F2,…,Fn}，若存在一个代换λ使得 F1λ=F2λ=…=Fnλ    ，则称λ为公式集F的一个合一，且称F1,F2,…,Fn是可合一的。
例如，设有公式集 F={P(x,y,f(y)),P(a,g(x),z)} 则下式是它的一个合一：
λ={a/x,g(a)/y,f(g(a))/z}    a/x：a代换x的意思，并不是a除x
一个公式集的合一一般不唯一。

定义3.4 设σ是公式集F的一个合一，如果对任一个合一θ都存在一个代换λ，使得θ=σ°λ 则称σ是一个最一般的合一。 最一般合一是唯一的。

求最一般合一

差异集：两个公式中相同位置处不同符号的集合。
例如：F1:P(x,y,z), F2:P(x,f(a),h(b)) 则D1={y,f(a)}, D2={z,h(b)}

求取最一般合一的算法：
1.令k=0,Fk=F, σk=ε。 ε是空代换。
2.若Fk只含一个表达式，则算法停止，σk就是最一般合一。
3.找出Fk的差异集Dk。
4.若Dk中存在元素xk和tk，其中xk是变元，tk是项，且xk不在tk中出现，则置：
  σK+1=σk°{tk/xk}
  Fk+1=Fk{tk/xk}
  k=k+1
然后转(2)。若不存在这样的xk和tk则算法停止。
5.算法终止，F的最一般合一不存在。

例如:
设 F={P(a,x,f(g(y))),P(z,f(z),f(u))} 求其最一般合一。
1.令F0=F, σ0=ε。 F0中有两个表达式，所以σ0不是最一般合一。
2.差异集D0={a,z} 。
3. σ1=σ0°{a/z}={a/z}     F1={P(a,x,f(g(y))),P(a,f(a),f(u))} 。
4.D1={x,f(a)} 。
5. σ2=σ1°{f(a)/x}={a/z,f(a)/x}     F2=F1{f(a)/x}={P(a,f(a),f(g(y))),P(a,f(a),f(u))} 。
6.D2={g(y),u} 。
7.σ3=σ2°{g(y)/u}={a/z,f(a)/x,g(y)/u}
8.F3=F2{g(y)/u}={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))} 。因为F3中只有一个表达式，所以就是最一般合一，即     {a/z,f(a)/x,g(y)/u}