개념
유니피케이션은 두 논리식을 같게 만들기 위해 변수에 값을 대입하는 과정이다. 술어 논리와 Prolog 추론에서 핵심 역할을 한다.
예시
P(x)와 P(a)가 있을 때 x에 a를 대입하면 두 식은 같아진다. 이처럼 변수에 적절한 값을 넣어 두 표현을 일치시키는 것이 유니피케이션이다.
치환 를 적용하면 다음이 성립한다.
일반적으로 유니파이어는 두 식을 같게 만드는 치환이다.
Prolog에서의 역할
Prolog는 질문을 받으면 관련 규칙을 찾고, 변수에 값을 대입해 목표를 증명한다. 이때 유니피케이션이 변수를 실제 상수나 다른 변수와 연결한다.