反ユニフィケーション

反ユニフィケーションとは、2つの与えられた記号式に共通の一般化を構築するプロセスである。ユニフィケーションと同様に、許可される式(用語とも呼ばれる)と、等しいと見なされる式に応じて分類できる。関数を表す変数が式で許可されている場合、そのプロセスは「高階反ユニフィケーション」と呼ばれ、そうでない場合は「一次反ユニフィケーション」と呼ばれる。一般化が各入力式に文字通り等しいインスタンスを持つ必要がある場合、プロセスは「構文的反ユニフィケーション」や「E-反ユニフィケーション」または「反ユニフィケーションモジュロ理論」と呼ばれる。