ユニフィケーション
項 s 0 , t 0 , ... , s n , t n {\displaystyle s_{0},t_{0},\ldots ,s_{n},t_{n}} についてのユニフィケーション問題 G {\displaystyle G} が G = { s 1 = ? t 1 , ... , s n = ? t n } {\displaystyle {\text{ }}G=\{s_{1}{\stackrel {\text{?}}{=}}t_{1},\ldots ,s_{n}{\stackrel {\text{?}}{=}}t_{n}\}} という潜在的等式の多重集合で表されるとき、そのアルゴリズムはそれらの式に以下に示す項書き換え規則を適用し、等価な形式である { x 1 = ? u 1 , ... , x m = ? u m } {\displaystyle \{x_{1}{\stackrel {\text{?}}{=}}u_{1},\ldots ,x_{m}{\stackrel {\text{?}}{=}}u_{m}\}} に変形しようとする。ここで、 x 0 , ... , x m {\displaystyle x_{0},\ldots ,x_{m}} は一意な変数である(1つの式の左辺に一度だけ現れ、他の部分には出現しない)。
2つの項 s と t があるとき、(統語論的)ユニフィケーションは s と t を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを s と t の単一子と呼ぶ。
理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの最大汎用単一子を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。
一階のユニフィケーションは、一階の項(変数記号や関数記号で構築される項)の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項(何らかの高階の変数を含む項)のユニフィケーションを指す。
特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。