归结原理-置换

1. 定义: 置换是一个形如{t1/a1,…, tn/an}的有限集,其中每个vi是变量,ti是不同于ai的项（常量、变量或函数）(ai≠ti). 当i≠j时，vi≠vj.

    无元素组成的置换称为空置换, 记为ε={};

2.表示：希腊字母θ，λ，σ表示 

   例如：θ＝{f(b)/x, a/y} 

   规则：将x置换成f(b)，y置换成a。

   注意：{x/x}, {y/f(x)}不是置换;

    被置换元素必是变量，置换元素是项;

    置换元素必不同于被置换元素;

    在一次置换中，针对同一元素的置换只能出现一次(单次置换的同时性);

3. 置换的乘法（复合）

设有两个置换θ={t1/x1,...,tn/xn}，λ={u1/y1,...,um/ym},置换的乘积θ● λ是一个新的置换

规则如下

*先做置换{t1λ/x1,...,tnλ/xn,u1/y1,...,um/ym};

*如果yj∈(x1,...,xn),   则删除uj/yj;

*如果tkλ=xk,         则删除tkλ/xk;

4.置换乘法的例子

     θ={f(y)/x,z/y}

     λ={a/x,b/y,y/z}

     θ●λ={f(y)●λ/x,z●λ/y,a/x,b/y,y/z} //分别对ti/xi, 进行与λ的复合

       ={f(b)/x,y/y,a/x,b/y,y/z} 

//根据置换定义，删去y/y，根据置换乘法规则2，删去a/x，b/y

       ={f(b)/x,y/z}

5.置换乘法的性质

(θ● λ)●μ=θ● (λ●μ) 成立

θ● λ=λ●θ 不一定成立