스콜렘 표준형
From Wikipedia, the free encyclopedia
수리논리학에서 스콜렘 표준형(Skolem normal form)은 보편 양화사만으로 이루어진 프리넥스 표준형 1차 논리식을 가리킨다.
모든 1차 논리식들은 스콜렘화(Skolemization)라는 과정을 통해 그 충족가능성(satisfiability)을 변화시키지 않은 채 스콜렘 표준형으로 변환될 수 있다. 여기서 결과의 논리식이 반드시 원래의 식과 동치인 것은 아니나, 서로 모델론적으로는 일치한다: 곧, 어느 한 쪽이 충족가능하다는 것과 다른 쪽이 충족가능하다는 것이 동치이다. 스콜렘화는 논리적 진술로부터 존재 양화사를 모두 제거해나가는 방식으로 이루어진다.