명제증명제

명제 미적분학 및 증명 복잡성에서 명제 증명 시스템(pps)은 고전 명제 증명 tautology를 증명하기 위한 시스템이다.

수학적 정의

pps는 모든 제안적 tautology(TAUT로 표기됨)의 집합인 다항식 시간 함수 P이다.^[1]A가 공식이라면 P(x) = A와 같은 x를 A의 P-proof라고 한다.pps를 정의하는 조건은 다음과 같이 나눌 수 있다.

• 완전성: 모든 명제적 태동학은 P-proof를 가지고 있다.
• 건전성: 명제 공식에 P-proof가 있다면 그것은 tautology이다.
• 효율성: P는 다항식 시간에 실행된다.

일반적으로 언어 L에 대한 교정 시스템은 범위가 L인 다항식 시간 함수다.따라서, 명제 증명 시스템은 TAUT를 위한 증명 시스템이다.

때때로 다음과 같은 대체 정의를 고려한다: pps는 두 개의 입력을 가진 증명 검증 알고리즘 P(A,x)로 주어진다.만약 P가 쌍(A,x)을 받아들인다면, 우리는 x가 A의 P-proof라고 말한다.P는 다항식 시간에 뛰어야 하며, 더욱이 A는 tautology일 경우에만 P-proof가 있다는 것을 보유해야 한다.

P가₁ 첫 번째 정의에 따른 pps인 경우 P₁(x) = A가 두 번째 정의에 따른 pps인 경우에만 P₂₂(A,x)로 정의된다.반대로 P가₂ 두 번째 정의에 따른 pps라면 P는 다음과₁ 같이 정의된다.

${\displaystyle P_{1}(\langle x,A\rangele )={\begin{case}A&{\text}{{p_{2}(A,x)\\top &{\text{otherwise}\end{case}}}}$

(P는₁ 쌍을 입력으로 취함)은 첫 번째 정의에 따른 pps로, 여기서 $\top {\displaystyle \mathrm{}}$ ${\displaystyle \top }$은 고정 tautology이다.

알고리즘 해석

두 번째 정의는 TAUT의 멤버십을 해결하기 위한 비결정론적 알고리즘으로 볼 수 있다.이것은 pps에 대한 초다항식 증명 크기를 증명하는 것이 그 pps에 기초한 특정 종류의 다항식 시간 알고리즘의 존재를 배제한다는 것을 의미한다.

예를 들어, 비둘기 구멍 원리의 분해능이 낮은 지수 증명 크기는 분해능에 기반한 어떤 알고리즘도 TAUT나 SAT를 효율적으로 결정할 수 없으며 비둘기 구멍 원리의 tautology에서 실패할 것임을 암시한다.이는 해상도에 기반한 알고리즘 등급이 현재의 명제적 증명 검색 알고리즘과 최신 산업용 SAT 해결사의 대부분을 포함하기 때문에 중요하다.

역사

역사적으로 프레지의 명제적 미적분은 최초의 명제적 증명 시스템이었다.명제 증명 시스템의 일반적인 정의는 스티븐 쿡과 로버트 A 때문이다. 레크쇼(1979년).^[1]

계산 복잡성 이론과의 관계

p-시뮬레이션의 개념을 사용하여 명제 증명 시스템을 비교할 수 있다.명제 증명 시스템 P는 다항 시간 함수 F가 있을 때 모든 x에 대해 P(F(x) = Q(x)가 되도록 Q(P ≤_pQ로 표기)를 시뮬레이션한다.^[1]즉, Q-proof x가 주어지면 다항식 시간에 동일한 tautology의 P-proof를 찾을 수 있다.P ≤_pQ와 Q ≤_pP일 경우, 증명 시스템 P와 Q는 p-등가형이다.There is also a weaker notion of simulation: a pps P simulates or weakly p-simulates a pps Q if there is a polynomial p such that for every Q-proof x of a tautology A, there is a P-proof y of A such that the length of y, y is at most p( x ). (Some authors use the words p-simulation and simulation interchangeably for either of these two concepts,보통 후자)

명제 증명 시스템은 다른 명제 증명 시스템을 모두 p-최적화하면 p-최적화라고 하며, 다른 pp를 모두 시뮬레이션하면 최적이다.명제 증명 시스템 P는 모든 tautology가 짧은(즉, 다항식 크기) P-proof를 갖는 경우 다항식 경계(슈퍼라고도 함)이다.

P가 다항식 경계이고 Q가 P를 시뮬레이션한다면 Q도 다항식 경계다항 경계다.

명제 tautologys의 집합인 TAUT는 coNP-완전 집합이다.명제증명제도는 TAUT의 회원 자격을 증명하는 제도다.다항 경계 제안 증명 시스템의 존재는 다항 크기 인증서를 가진 검증자가 있다는 것을 의미한다. 즉, TAUT는 NP에 있다.사실 이 두 진술은 동등하다. 즉, 복잡도 등급 NP와 coNP가 동일한 경우에만 다항 경계 제안 증명 시스템이 있다.^[1]

시뮬레이션 또는 p-시뮬레이션에 따른 증명 시스템의 일부 동등성 클래스는 경계 산술 이론과 밀접하게 관련되어 있다; 그것들은 본질적으로 경계 산술의 "비균일" 버전이며, 회로 클래스가 자원 기반 복잡성 클래스의 균일하지 않은 버전인 것과 같은 방식이다."Extended Frege" 시스템(정의에 의한 새로운 변수 도입 허용)은 예를 들어 다항식 경계 시스템에 이와 같은 방식으로 대응한다.차례로 경계 산술은 회로 기반 복잡도 등급에 해당하는 경우, 하한 결과와 분리를 일치시키는 것과 같은 증명 시스템 이론과 회로 계열의 이론 사이에는 종종 유사성이 있다.예를 들어, 부존재 크기의 $A{\displaystyle {\mathbf{}}^{}}$ C ${\displaystyle {\mathrm{}}^{}}$ ${\$ 회로$$ 제품군에 의해 카운팅을 수행할 수 없듯이, 비둘기 구멍 원리와 관련된 많은 tautology는 한계 심층 공식(특히 분해능 기반 시스템이 아닌)에 기초한 증명 시스템에서 하위 증빙을 가질 수 없다.y는 오직 깊이 1 공식에 대해서만).

제안적 증명 시스템의 예

연구된 명제 증명 시스템의 몇 가지 예는 다음과 같다.

• 제안적 해결 및 DPLL 알고리즘과 같은 다양한 제한 및 확장
• 자연공제
• 시퀀스 미적분학
• 프레게 시스템
• 확장 프레지 시스템
• 다항식 미적분학
• Nullstellensatz 시스템
• 절단면법

참조

추가 읽기

• Samuel Bushs(1998), "증거 이론 소개"에서: 증명 이론 핸드북(Ed. S.R.Buss), Exvier(1998)
• P. P. Pudlahk(1998), "증거의 길이"에서: 증명 이론 핸드북(ed. S.R.Buss), 엘스비에(1998)
• Beame과 T. 피타시(1998년).명제 증명 복잡성: 과거, 현재 및 미래.기술 보고서 TR98-067, 전산 복잡성에 관한 전자 콜로키움.
• Nathan Segerlind(2007) "Proposal Proofs의 복잡성", 기호논리 13(4): 417–481
• J. Krajichek(1995), Bounded Mathry, Proposal Logic, and Complexity 이론, 캠브리지 대학 출판부.
• J. Krajichek, Proof complexity in: Proc.제4차 유럽 수학 대회(ed)A. Laptev), 취리히 EMS, 221–231, (2005)페이지.
• J. Krajichek, 제안 증명 복잡성 I. 및 증명 복잡성 및 산술.
• Stephen Cook and Phuong Nguyen, Cambridge University Press, 2010년 초안)
• 로버트 레코우 박사 학위논문, 1975년 발의안 미적분학에서 증명된 길이에 대하여.

외부 링크

• 증명 복잡성