一致化

替換：
替換為將變數對映到詞的一對一函數，其表示如下：
{X1/t1, X2/t2,...,Xn/tn}

一致化：
令 s 及 t 為式，若存在替換 T 使得 sT = tT 語義相等，則 s 及 t可以一致化，而該替換 T 稱為 s 及 t 之一致子。

形式一致化問題：

找出可使一組等式集合 ES 之合取 t0 = u0 & t1 = u 1 &...& tn = un 語義相等之替換 S。
此替換稱為該等式集合之一致子。

解式：
為一組等式，等式左側均為不同變數，且不會出現在右側中。
[$x=x,$f=f(x o),$q=q,$s=s]
即為一組解式。

一致化為給定一組等式，並將其轉換成解式之過程。

1.下面形式則表示無法一致化
1.1. f = g 其中f及g 是相異原子。
1.2. f = g 其中f為複合子及g是原子，f為原子及g是複合子。
1.3. f(...) = g(...) 其中f及g 是相異函子。
1.4. f(a1, a2, ..., aN) = g(b1, b2, ..., bM) 其中N及M數目不同。
2.$X=$X 其中$X均為變數，則刪除此等式
3.a=a 其中a均為元式，則刪除此等式4. f(a1, a2, ..., aN) = f(b1, b2, ..., bN) 則用 ai = bi 等式組取代
5.t = X 其中 X 為變數而 t為非變數，則以 X = t取代6.X = t 其中 X 為變數而 t為非變數，且 X 未在 t 中，而存在其它等式中，後把其它等式出現的X 以 t 取代。
7.X = t 其中 X 為變數而 t為非變數，且 X 在 t 中，則因正向變數檢查而無法一致化。
8.若無其它步驟可套用，則一致化成功。