人工智能
置换与合一
置换
在一个谓词公式中用项去替换变量。
置换是形如 { t1/x1, t2/x2, …, tn/xn } 的有限集合。

其中：
t1,t2,…,tn是项；
x1,x2,…,xn是互不相同的变元；
ti/xi表示用ti替换xi。
并且要求ti与xi不能相同，xi不能循环地出现在另一个ti中。

比如：{a/x, c/y, f(b)/z} 是一个置换
{g(y)/x, f(x)/y} 不是一个置换.

因为置换的目的是用其它的变量、常量、函数替换谓词公式中的某个变量，使其不再出现在公式中，{ f(y)/x, g(x)/y } 中出现了 x，y 的循环替换，结果既不能消去x也不能消去 y，所以不是一个置换。不符合定义的要求。

置换常用罗马字符表示：如 θ、σ、 α、 λ

合一
合一是寻找置换，使得2个谓词或谓词公式一致。
合一和可合一公式
设有公式集F={F1, F2,…,Fn}，若存在一个置换θ，可使：F1θ=F2θ=…=Fnθ。
则称θ是F的一个合一置换。
称F1,F2,…,Fn是可合一的公式。
可合一公式集合的合一置换往往不止一个。
例：公式集：F={ P( x, f(y), B), P( x, f(B), B) }
置换 θ={ A/x, B/y } 是一个合一置换。因为：
P( x, f(y), B ) θ = P( A, f(B), B )
P( x, f(B), B) θ = P( A, f(B), B )
置换 λ={ g(w)/x, B/y } 是另一个合一置换。
最一般（通用）合一者（mgu）
如果 F={F1, F2,…,Fn}是一个可合一公式集合，设σ是公式集F的一个合一置换。
即F1σ=F2σ=…=Fn-1σ=Fnσ
如果对F的任一个合一者(合一置换)θ都存在一个置换λ，使得θ=σλ，则称σ是F的最一般合一者。
一个公式集的最一般合一者是唯一的