프리넥스 표준형 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]에서 '''프리넥스 표준형'''(prenex標準型, {{llang|en|prenex normal form}})은 모든 한정 기호가 앞에 와 있는 [[1차 논리]] 공식의 형태이다.

== 정의 ==
'''프리넥스 표준형'''인 [[1차 논리|1차]] [[술어 논리]] 공식은 다음과 같은 형태의 공식 <math>\phi</math>이다.
:<math>\phi=\phi_{\text{prefix}}\phi_{\text{matrix}}</math>
여기서
* <math>\phi_{\text{prefix}}</math>는 기호 <math>\exists</math>와 <math>\forall</math> 및 변수만을 포함하는 문자열이다. 특히, <math>\land</math>나 <math>=</math> 및 기타 연산·관계를 포함하지 않는다. 이를 <math>\phi</math>의 '''접두사'''({{llang|en|prefix|프리픽스}})라고 한다.
* <math>\phi_{\text{matrix}}</math>는 기호 <math>\forall</math>을 포함하지 않는 문자열이다. 즉, 변수와 <math>\lnot</math>, <math>\land</math>, <math>=</math> 및 기타 연산·관계만으로 구성된다. 이를 <math>\phi</math>의 '''매트릭스'''({{llang|en|matrix}})라고 한다.

== 알고리즘 ==
모든 1차 논리 공식은 프리넥스 표준형인 명제와 [[동치]]이며, 주어진 공식과 동치인 프리넥스 표준형 공식은 다음과 같이 찾을 수 있다. 편의상, 모든 [[논리합]](<math>\lor</math>)이나 함의(<math>\implies</math>)를 [[논리곱]](<math>\land</math>) 및 부정(<math>\lnot</math>)으로 나타내자. 그렇다면 1차 논리 공식을 다음과 같이 변환시킨다.
* <math>(\forall x\colon\phi)\land\psi</math>를 <math>\forall x'\colon(\phi[x'/x]\land\psi)</math>로 변환시킨다. 여기서 <math>x'</math>은 <math>\psi</math>에 포함되지 않는 임의의 변수이다.
*  <math>(\exists x\colon\phi)\land\psi</math>를 <math>\exists x'\colon(\phi[x'/x]\land\psi)</math>로 변환시킨다. 여기서 <math>x'</math>은 <math>\psi</math>에 포함되지 않는 임의의 변수이다.
* <math>\lnot\exists x\colon\phi</math>를 <math>\forall x\colon\lnot\phi</math>로 변환시킨다.
* <math>\lnot\forall x\colon\phi</math>를 <math>\exists x\colon\lnot\phi</math>로 변환시킨다.

== 역사와 어원 ==
프리넥스({{llang|en|prenex}})라는 단어는 {{llang|la|praenexus|프라이넥수스}}(묶인, 고정된)에서 왔다. 이 용어는 [[다비트 힐베르트]]와 [[파울 베르나이스]]의 1938년 저서 《수학의 기초》({{llang|en|Grundlagen der Mathematik}})에서 최초로 사용하였다.

== 같이 보기 ==
* [[1차 논리]]
* [[스콜렘 표준형]]

== 외부 링크 ==
* {{매스월드|id=PrenexNormalForm|title=Prenex normal form}}
* {{웹 인용|url=http://www.xamuel.com/prenex/|제목=Prenex Normal Form Generator|이름=Sam|성=Alexander|언어=en|확인날짜=2015-01-01|보존url=https://web.archive.org/web/20140908181042/http://www.xamuel.com/prenex/|보존날짜=2014-09-08|url-status=dead}}

[[분류:논리학]]