문서의 임의 삭제는 제재 대상으로, 문서를 삭제하려면 삭제 토론을 진행해야 합니다. 문서 보기문서 삭제토론 자동정리증명 (문단 편집) ==== Skolemization ==== Skolemization은 만든 사람의 이름인 Skolem에서 따왔다. [math( \forall x_1, \forall x_2, \cdots, \forall x_n, \exists y, R( x_1, x_2, \cdots, x_n, y) \implies \forall x_1, \forall x_2, \cdots, \forall x_n, R( x_1, x_2, \cdots, x_n, f(x_1, x_2, \cdots, x_n)) )] 즉 어떤 [math(f)]라는 새로운 함수를 정의해 [math(\exists)]가 붙어있는 [math(y)]를 이 함수와 다른 [math( x_1, x_2, \cdots, x_n)]로 표현하겠다는 것이다. 어찌보면 당연해 보이지만 증명은 간단하지 않으며 1차 논리의 모델을 이용하여 증명한다.저장 버튼을 클릭하면 당신이 기여한 내용을 CC-BY-NC-SA 2.0 KR으로 배포하고,기여한 문서에 대한 하이퍼링크나 URL을 이용하여 저작자 표시를 하는 것으로 충분하다는 데 동의하는 것입니다.이 동의는 철회할 수 없습니다.캡챠저장미리보기