第二章 归结推理方法

　　2.4.1 置换与合一
　　置换是形为　
　　　　　　　{t1/v1,…,tn/vn}
的一个有限集。其中vi是变量而ti是不同于vi的项(常量、变量、函数)，且vi≠vj(i≠j),i,j=1,2,…,n。
　　例如{a/x,b/y,f(x)/z},{f(z)/x,y/z}都是置换。
　　不含任何元素的置换为空置换，以ε表示。
　　置换可作用于某个谓词公式上，也可作用于某个项上。令置换θ＝{t1/v1,… ,tn/vn}，而E是一谓词公式，那么θ作用于E，就是将E中出现的变量vi均以ti代入(i=1, …,n),结果以Eθ表示，并称为E的一个例。θ作用于项t也是将t中出现的变量vi以ti代入(i=1, …,n),结果以t・θ表示。
例题 例:
  　　θ＝{a/x,f(b)/y,u/z}
　　E＝P(x,y,z)
　　t=g(x,y)
　那么　Eθ＝P(a,f(b),u)
　　　　tθ=g(a,f(b))
　显然，若E是子句集S的一个子句，置换θ的v1,…,vn含有E的所有变量，ti又是H的元素时，Eθ便是S的子句E的基例。
　常使用的置换间的运算是置乘法（合成）。
　若　θ＝{t1/x1,…,tn/xn}
　　　λ＝{u1/y1,…,um/ym}
　置换的乘积θ・λ是个新的置换，作用于E相当于先θ后λ对E的作用。为此可如下定义
　先作置换
　　　{t1・λ/x1,…,tnλ・/xn ,u1/y1,… ,um/ym}
　若　yi∈{x1,…,xn}时，先从中删除ui/yi
　　　ti・λ=xi 时，再从中删除ti・λ/xi
所得的置换称作θ与λ的乘积，记作θ・λ。
例题 例:
  　　θ＝{f(y)/x,z/y}
　　λ＝{a/x, b/y, y/z}
　求 λ・θ。
　先作置换　{f(y)・λ/x,z・λ/y,a/x,b/y,y/z}={f(b)/x,y/y,a/x,b/y,y/z}
　先删除　a/x,b/y,再删y/y得
　　　θ・λ ＝{f(b)/x,y/z}
　当　E =P(x,y,z) 时，
　　　E(θ・λ)＝P(f(b),y,y)
　而　Eθ = P(f(y),z,z)
　　　(Eθ)λ＝P(f(b),y,y)=E(θ・λ)
　　　一般地说有
　　　(θ・λ)・μ=θ・(λ・μ)
　　　ε・θ＝θ・ε＝θ
　但交换律是不成产的。
　下面介绍合一的概念，设有公式集合{E1,…,Ek}和置换θ，使
　　　E1θ= E2θ= …=Ekθ
　便称E1,…,Ek是可合一的，且θ称为合一置换。
　若E1,…,Ek有合一置换σ且对E1,…,Ek的任一合一置换θ都有置换λ存在使得
　　　θ =σ・λ
　便说σ是 E1,…,Ek 的最一般合一置换，记作 mgu 。
例题 例1:
  　E1＝P(a ,y) E2=(x,f(b))
　是可合一的，有合一置换θ ={a/x,f(b)/y},且θ也是E1，E2 的 mgu 。
例题 例2:
  　E1=P(x) E2=P(f(y))
　是可合一的，有合一置换θ＝{f(a)/x,a/y} 但θ不是E1，E2 的 mgu 。
　σ＝{f(y)/x}方是E1，E2 的mgu，也可以说E1，E2 的 mgu 是最简单的合一置换。
例题 例3:
  　E1＝P(x) E2=P(y)
显然{y/x}和{x/y}都是E1，E2 的 mgu，这说明E1，E2 的 mgu 并不是唯一的。
　对给定的公式E1，E2 来说，采用逐一比较找出不一致，并作相应的合一置换的办法便可求得 mgu 。
　mgu 算法
　(1) 令W={E1，E2}
　(2) 令K＝0，W0＝W，σ0＝ε
　(3) 如果Wk已合一，停止，σk =mgu
　　　否则找不一致集Dk
　(4) 若Dk中存在元素vk，tk，其中vk不出现于tk中做(5)，否则不可合一 。
　(5) 令σk+1=σk・{tk/vk}Wk+1=Wk{tk/vk}=Wσk+1
　(6) k+1→转(3)
　可证明若E1，E2可合一，算法必停于(3)。
例题 例:
  　W＝{P(a,x,f(g(y))),P(z,f(a),f(u))}
其中 E1=P(a,x,f(g(y))),E2=P(z,f(a),f(u))
　求　E1，E2的 mgu 。依算法
　(1) W＝{P(a,x,f(g(y)))，P(z,f(a),f(u))}
　(2) σ0＝ε，W0＝W，
　(3) W0未合一，从左到右找不一致集，有D0＝{a,z}。
　(4) 取v0＝z,t0＝a。
　(5) 令 σ1＝σ0・(t0/v0）＝{a/z}
　　　　 W1＝W0 σ1＝{P(a,x,f(g(y)))，P(a,f(a),f(u))}
　(3)' W1 未合一，从左到右找不一致集，有D1={x,f(a)}
　(4)' 取v1 =x t1=f(a)
　(5)' 令 σ2=σ1・{f(a)/x}={a/z,f(a)/x}
　　　　　W2＝W1σ2＝{P(a,a,f(g(y)))，P(a,f(a),f(w))}
　(3)" W2未合一，从左到右找不一致集，有D2={g(y),u}
　(4)" 取v2=u，t2=g(y)
　(5)" 令 σ3=σ2・{g(y)/u}={a/z,f(a)/x,g(y)/u}
　　　　　W3＝W2σ3＝{P(a,f(a),f(g(y)))，P(a,f(a),f(g(y)))}
　(3)'" W3 已合一，这时σ3={a/z,f(a)/x,g(y)/u}
　便是E1，E2 的 mgu 。
　算法的第4步，当出现不存在vk 如 W＝{P(a,b,c),P(d,b,c)},或不存在tk如W＝{P(a,b),P(x,y,z)},或出现不一致集为{x,f(x)}形。这都会导致不可合一。