프리넥스 표준형

수리논리학에서 프리넥스 표준형(prenex標準型, 영어: prenex normal form)은 모든 한정 기호가 앞에 와 있는 1차 논리 공식의 형태이다.

정의

프리넥스 표준형인 1차 술어 논리 공식은 다음과 같은 형태의 공식 $\phi$ 이다.

\phi =\phi _{\text{prefix}}\phi _{\text{matrix}}

여기서

$\phi _{\text{prefix}}$ 는 기호 $\exists$ 와 $\forall$ 및 변수만을 포함하는 문자열이다. 특히, $\land$ 나 $=$ 및 기타 연산·관계를 포함하지 않는다. 이를 $\phi$ 의 접두사(영어: prefix 프리픽스^[*])라고 한다.
$\phi _{\text{matrix}}$ 는 기호 $\forall$ 을 포함하지 않는 문자열이다. 즉, 변수와 $\lnot$ , $\land$ , $=$ 및 기타 연산·관계만으로 구성된다. 이를 $\phi$ 의 매트릭스(영어: matrix)라고 한다.

알고리즘

모든 1차 논리 공식은 프리넥스 표준형인 명제와 동치이며, 주어진 공식과 동치인 프리넥스 표준형 공식은 다음과 같이 찾을 수 있다. 편의상, 모든 논리합( $\lor$ )이나 함의( $\implies$ )를 논리곱( $\land$ ) 및 부정( $\lnot$ )으로 나타내자. 그렇다면 1차 논리 공식을 다음과 같이 변환시킨다.

$(\forall x\colon \phi )\land \psi$ 를 $\forall x'\colon (\phi [x'/x]\land \psi )$ 로 변환시킨다. 여기서 $x'$ 은 $\psi$ 에 포함되지 않는 임의의 변수이다.
$(\exists x\colon \phi )\land \psi$ 를 $\exists x'\colon (\phi [x'/x]\land \psi )$ 로 변환시킨다. 여기서 $x'$ 은 $\psi$ 에 포함되지 않는 임의의 변수이다.
$\lnot \exists x\colon \phi$ 를 $\forall x\colon \lnot \phi$ 로 변환시킨다.
$\lnot \forall x\colon \phi$ 를 $\exists x\colon \lnot \phi$ 로 변환시킨다.

역사와 어원

프리넥스(영어: prenex)라는 단어는 라틴어: praenexus 프라이넥수스^[*](묶인, 고정된)에서 왔다. 이 용어는 다비트 힐베르트와 파울 베르나이스의 1938년 저서 《수학의 기초》(영어: Grundlagen der Mathematik)에서 최초로 사용하였다.

같이 보기

외부 링크

Weisstein, Eric Wolfgang. “Prenex normal form”. 《Wolfram MathWorld》 (영어). Wolfram Research.
Alexander, Sam. “Prenex Normal Form Generator” (영어). 2014년 9월 8일에 원본 문서에서 보존된 문서. 2015년 1월 1일에 확인함.