ユニフィケーション

ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つのが同一または同等であることを示すを求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。 なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。 主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。 ユニフィケーションアルゴリズムはジャック・エルブランによって最初に発見されたが、ユニフィケーションを初めて形式的に研究したのはで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。