合    一 

 1、合一的定义

      在定理证明过程中，经常需要对量化的公式进行匹配操作，这就需要通过变量置换使两个公式一致起来，这个过程称为合一。  

  2、重要概念

    一个表达式的项可以是常量、变量或函数，合一就是寻找项对变量的置换而使表达式一致的过程。例如，为了使公式("x)W(x)与W(A)匹配，我们可以用常量A代替变量x，从而使两个公式一致。置换的结果称为该表达式通过置换得到的例。例如，表达式P[x,f(y),b]可以通过不同的置换得到不同的例：

    P[x,f(w),b]          变量®变量

    P[x,f(A),b]          常量®变量

    P[g(z),f(y),b]       函数®变量

    P[c,f(A),b]          常量®变量

上面的最后一个例中没有变量，称为基例。

    我们用有序对的集合S={t1/v1,t2/v2,...,tn/vn}表示置换，其中ti/vi表示在表达式中用ti代替vi。对一个变量在表达式中的每次出现，都应当用同一各项来代替它。而且，一个变量不能用含有同一个变量的项来代替，例如用f(x)代替x是不允许的。上述四个利所用的置换可表示为

    s1={z/x,w/y}

    s2={A/y}

    s3={g(z)/x}

    s4={c/x,A/y}

    用置换s作用于表达式E所得到的例，记为Es，如：

         P[x,f(w),b]= P[x,f(y),b]s1

    当用两个置换s1和s2依次作用于一个表达式时，可以将两个置换s1和s2组合成为一个置换称为s1与s2的合成，记为s1s2。

 3、合成的步骤

    我们用一个例子来说明。将量个置换

        s1={g(x,y)/z}

        s2={A/x,b/y,c/w,D/z}

合成的步骤如下：    

   （1）把s1作用于s2，得到g(A,b)/z

  （2）把s1中所没有的那些s2中的对加入到s1，则s1即成为s1与s2合成。因此有

     s1s2={g(A,b)/z,A/x,b/y,c/w}

                                            下接