反ユニフィケーション

ウィキペディア

反ユニフィケーション

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/12 08:10 UTC 版)

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