문서의 임의 삭제는 제재 대상으로, 문서를 삭제하려면 삭제 토론을 진행해야 합니다. 문서 보기문서 삭제토론 단일화 (문단 편집) == 논리 용어 == 1차 논리에서의 변수는 초변수(meta variable)로 생각할 수 있는데 이 초변수의 연립방정식을 푸는 것을 단일화라고 하고 그 해를 단일화 기호(unifier)라고 부른다. 예를 들어 [math( f(X) = f(f(Z)) )]라는 단일화 문제(Unification problem)가 있다면 이 둘이 같아지도록 초변수 [math(X\text{ 와 } Z)]를 설정해야 할 것이다. 그렇다면 [math(X=f(c), Z=c)]인 상황을 생각해 볼 수 있다. 그런데 이외에도 [math(X=f(f(c)), Z=f(c))]인 경우에도 이 연립방정식[* 1의 예시에서는 이해를 돕기위해 단순화 시켰기 때문에 그냥 방정식처럼 보이지만 실제로는 연립방정식의 해를 구하는 것이다.]의 해가 될 수 있다. 따라서 이렇게 많은 해 중에서 의미있는 것을 구별해내기 위해 most general unifier라는 개념을 도입하였다. most general unifier는 어떤 단일화 문제의 모든 답들의 근간이 될 수 있는 답을 말한다. 예를 들어 아까의 예시의 경우 most general unifier는 [math(X=f(Y),Z=Y)]다. 그러면 초변수 [math(Y)]에 들어가는 값에 따라 전부 답이 될 수 있는 가장 기초적인 답이라고 할 수 있다.저장 버튼을 클릭하면 당신이 기여한 내용을 CC-BY-NC-SA 2.0 KR으로 배포하고,기여한 문서에 대한 하이퍼링크나 URL을 이용하여 저작자 표시를 하는 것으로 충분하다는 데 동의하는 것입니다.이 동의는 철회할 수 없습니다.캡챠저장미리보기