2.4.1 合一和置换
置换：置换可以简单的理解为是在一个谓词公式中用置换项去置换变量。
定义：
置换是形如{t
1
/x
1
, t
2
/x
2
, …, t
n
/x
n
}的有限集合。其中，x
1
, x
2
, …, x
n
是互不相同的变量，t
1
, t
2
, …, t
n
是不同于x
i
的项（常量、变量、函数）；t
i
/x
i
表示用t
i
置换x
i
，并且要求t
i
与x
i
不能相同，而且x
i
不能循环地出现在另一个t
i
中。