| 수학기초론 Foundations of Mathematics | |||
| {{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | 다루는 대상과 주요 토픽 | ||
| 수리논리학 | 논리 · 논증{귀납논증 · 연역논증 · 귀추 · 유추} · 공리 및 공준 · 증명{증명보조기 · 자동정리증명 · 귀류법 · 수학적 귀납법 · 반증 · 더블 카운팅 · PWW} · 논리함수 · 논리 연산 · 잘 정의됨 · 조건문(조각적 정의) · 명제 논리(명제 · 아이버슨 괄호 · 역 · 이 · 대우) · 양상논리 · 술어 논리(존재성과 유일성) · 형식문법 · 유형 이론 · 모형 이론 | ||
| 집합론 | 집합(원소 · 공집합 · 집합족 · 곱집합 · 멱집합) · 관계(동치관계 · 순서 관계) · 순서쌍(튜플) · 서수(하세 다이어그램 · 큰 가산서수) · 수 체계 · ZFC(선택공리) · 기수(초한기수) · 절대적 무한 · 모임 | ||
| 범주론 | 범주 · 함자 · 수반 · 자연 변환 · 모나드 · 쌍대성 | ||
| 계산가능성 이론 | 계산 · 오토마타 · 튜링 기계 · 바쁜 비버 · 정지 문제 · 재귀함수 | ||
| 정리 | |||
| 드모르간 법칙 · 대각선 논법 · 러셀의 역설 · 거짓말쟁이의 역설 · 뢰벤하임-스콜렘 정리 · 슈뢰더-베른슈타인 정리 · 집합-부분합 정리 · 퍼스의 항진명제 · 굿스타인 정리 · 완전성 정리 · 불완전성 정리(괴델 부호화) · 힐베르트의 호텔 · 연속체 가설 · 퍼지 논리 | |||
| 기타 | |||
| 예비사항(약어 및 기호) · 추상화 · 벤 다이어그램 · 수학철학 | |||
| 틀:논리학 · 틀:이산수학 · 틀:이론 컴퓨터 과학 · 철학 관련 정보 · 논리학 관련 정보 · 수학 관련 정보 | }}}}}}}}} | ||
| '''이론 컴퓨터 과학 {{{#!wiki style="display: inline-block; font-family:Times New Roman, serif;font-style:italic"''' | |||||
| {{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | <colbgcolor=#a36> 이론 | ||||
| 기본 대상 | 수학기초론{수리논리학(논리 연산) · 계산 가능성 이론 · 범주론 · 집합론} · 이산수학(그래프 이론) · 수치해석학 · 확률론 및 통계학 · 선형대수학 | ||||
| 다루는 대상과 주요 토픽 | |||||
| 계산 가능성 이론 | 재귀함수 · 튜링 머신 · 람다대수 · 처치-튜링 명제 · 바쁜 비버 | ||||
| 오토마타 이론 | FSM · 푸시다운 · 튜링 머신(폰노이만 구조) · 정규 표현식 · 콘웨이의 생명 게임 · 형식언어 | ||||
| 계산 복잡도 이론 | 점근 표기법 · 튜링 기계^고전, 양자, 비결정론적, 병렬 임의접근 기계^ · 알고리즘 · 자료구조 · 알고리즘 패러다임(그리디 알고리즘, 동적 계획법) | ||||
| 정보이론 | 데이터 압축(무손실 압축 포맷 · 손실 압축 포맷) · 채널 코딩(채널 용량) · 알고리즘 정보 이론(AIT) · 양자정보과학 | ||||
| 프로그래밍 언어이론 | 프로그래밍 언어(함수형 언어 · 객체 지향 프로그래밍 · 증명보조기) · 메타 프로그래밍 · 유형 이론 · 프로그래밍 언어 의미론 · 파싱 · 컴파일러 이론 | ||||
| 주요 알고리즘 및 자료구조 | |||||
| 기초 | 정렬 알고리즘 · 순서도 · 탐색 알고리즘 | ||||
| 추상적 자료형 및 구현 | 배열^벡터^ · 리스트^연결 리스트^ · 셋(set)^레드-블랙 트리, B-트리^ · 우선순위 큐^힙, 피보나치 힙^ | ||||
| 수학적 최적화 | 조합 최적화 | 외판원 순회 문제 · 담금질 기법 · 유전 알고리즘 · 기계학습 | |||
| 볼록 최적화 | 내부점 방법 · 경사하강법 | ||||
| 선형계획법 | 심플렉스법 | ||||
| 계산 수론 및 암호학 | 밀러-라빈 소수판별법 · Pollard-rho 알고리즘 · 쇼어 알고리즘 · LLL 알고리즘 · 해시(MD5 · 암호화폐 · 사전 공격(레인보우 테이블) · SHA) · 양자 암호 | ||||
| 대칭키 암호화 방식 | 블록 암호 알고리즘(AES · ARIA · LEA · Camellia) · 스트림 암호 알고리즘(RC4) | ||||
| 공개키 암호화 방식 | 공개키 암호 알고리즘(타원 곡선 암호 · RSA) · 신원 기반 암호 알고리즘(SM9) | ||||
| 계산기하학 | 볼록 껍질 · 들로네 삼각분할 및 보로노이 도형^Fortune의 line-sweeping 알고리즘^ · 범위 탐색^vp-tree, R-tree^ · k-NN | ||||
| 그래프 이론 | 탐색^BFS, DFS, 다익스트라 알고리즘, A* 알고리즘^ · 에드몬드-카프 · 크루스칼 알고리즘 · 위상 정렬 · 네트워크 이론 | ||||
| 정리 | |||||
| 정지 문제대각선 논법 · 암달의 법칙 · P-NP 문제미해결 · 콜라츠 추측미해결 | |||||
| 틀:이산수학 · 틀:수학기초론 · 틀:컴퓨터공학 | }}}}}}}}} | ||||
이 문서는 다음의 내용을 이미 숙지하고 있고 이해하고 있다 가정하고 작성된 문서입니다. 만약 이 중에 하나라도 이해를 하지 못한 비전공자께서는 다음의 내용들을 충분히 숙지 후 문서를 읽어주시기 바랍니다.
- 자연연역 (natural deduction)
- 1차 논리 (first order logic)
- NP
1. 개요
自動定理證明 / automated theorem proving자동정리증명은 주어진 논리를 증명하는 알고리즘이다. 단, 증명불가능한 문제[1]는 고려하지 않는다. 예를 들어 [math( \left( A \Rightarrow B \right) \land \left( B \Rightarrow C \right) \vdash \left( A \Rightarrow C \right) )]와 같은 논리를 컴퓨터[2]가 자동으로 증명 또는 반증해주는 것이다. 수학적 증명에 대한 자동화된 추론은 컴퓨터과학 발전의 주요 원동력이었다.
2. 정의
어떤 문제는 language로 정의될 수 있는데 즉, 어떤 문제를 [math( L : \left\{ 0,1 \right\} ^* \to \left\{ True, False \right\} )]로 쓸 수 있다. 그렇다면 자동정리증명문제는 다음과 같이 정의할 수 있을 것이다.증명 또는 반증이 가능한 language인 [math( L : \left\{ 0,1 \right\} ^* \to \left\{ True, False \right\} )]들의 집합을[math( \mathcal{P} )]라고 하자. 그러면 자동정리증명 알고리즘은 [math(f : \mathcal{P} \to \left\{ True, False\right\})]로 표현될 수 있다. 만약 어떤 논리 [math(p)]가 [math(f(p)=True)]를 만족한다면 논리 [math(p)]는 증명됐다는 것을 의미한다.
자동정리증명은 자동명제판별과 다르다. 어떤 명제의 True/False를 나누는 것은 model의 관점이지만 자동정리증명은 axiom을 이용한 proof system의 관점이다. 다만 일차논리는 괴델의 완전성정리에 의해 이 두개가 같은 의미를 가진다.
3. 복잡도
자동정리증명의 증명자(certifier)는 자동증명검증(automated proof verification)로 다항시간 알고리즘을 가진다. 이는 심지어 이미 구현된 사례(예시: Coq)까지 있기 때문에 굉장히 자명하다. 따라서 자동정리증명은 NP의 정의에 따라 NP문제임을 쉽게 알 수 있다.또 명백하게 SAT문제로부터 환원(reduction)이 가능하므로 대표적인 NP-complete문제임을 쉽게 알 수 있다.
4. 알고리즘
자동정리증명의 증명 방법은 귀류법을 이용한다[3]. 직접 증명하는 것이 아니라 귀류법을 사용하는 이유는 직접 증명하는 것은 공리(axiom)를 이용할 때 특별한 규칙이나 목표를 만들기 어려우나 귀류법을 사용하면 우리의 가정에 모순이 생겼음을 보이기만 하면 되므로 쉽다.기본적으로 자동정리증명은 해결 규칙(resolution rule)에 기반한다. 해결규칙은 논리곱 정규형(conjunctive normal form, 이하 CNF)의 상황에서 쓰일 수 있는 유용한 규칙인데 이를 사용하기 위해서는 주어진 입력을 CNF로 바꾸어야한다. CNF로 바꾸는 방법은 목표로 하는 논리의 범위에 따라 다르다. 이 문서는 1차 논리까지만 다룬다. 실제로 사용을 하기 위해서는 최소한 2차 논리 이상을 다룰 수 있어야 한다. 왜냐하면 기본적으로 많이 사용되는 자연수 분야의 공리인 페아노 공리계(Peano Axiom)는 전부 1차 논리인데 수학적 귀납(mathematical induction principle)이 무한한 1차 논리(infinite first order) 즉, 유한한 개수의 공리로 구성할 수 없다. 따라서 2차 논리를 빌려와야 유한개의 공리로 공리계를 구성할 수 있는데 그 표현은 다음과 같다.
[math( \displaystyle \forall \phi \ \left( \phi (0) \land \left( \forall x \ \phi (x) \Rightarrow \phi (S(x)) \right) \right) \Rightarrow \left( \forall x \ \phi (x) \right) )]
이로인해 실제로 ATP를 자연수 분야에서라도 쓰려면 2차 논리 이상은 다룰 수 있어야만 한다.
4.1. 0차 논리
먼저 0차 논리는 굉장히 쉽게 바꿀 수 있다. And, Or, Not 게이트를 하나의 literal에 대응시켜 변환하는 Tseitin(또는 Tseytin) transformation을 사용하면 선형시간(linear time)안에 주어진 입력을 CNF로 바꾸어준다. 이 CNF를 이용하여 resolution단계를 거쳐 실제로 이 CNF가 만족불가능(unsatisfiable)한지를 확인하여 만족불가능하면 이는 모순이 생겼음을 의미하고 귀류법을 통해 원래 명제를 증명한 것이다.4.1.1. Propositional Resolution
0차 논리는 굉장히 쉬워 해결규칙도 한 가지뿐인데 그것이 propositional resolution이다. propositional resolution은 다음의 추론 규칙을 기반으로 한다.[math( \displaystyle { \Gamma \vdash A \lor C \quad \Gamma \vdash B \lor \neg C \over \Gamma \vdash A \lor B } )]
이 규칙을 이용하다보면 만약 명제가 증명가능할 경우 마지막에 [math( A \land \neg A )]를 얻게 되고 이렇게 되면 이 전체 논리곱 정규형은 항상 거짓(false)가 된다. 따라서 귀류법에 의하여 이 명제는 참이 되는 것이다.
4.2. 1차 논리
1차 논리는 훨씬 복잡한데 그 이유는 0차 논리에서 허용하지 않던 정량자(quantifier ; [math(\forall, \exists)])를 허용하기 때문이다. 정량자로 인해서 변수가 생겨나게 되고 이로인해 자연연역을 적용할 수 있는 무한히 많은 가능성이 생기게 된다. 그래서 이를 해결하기 위해 여러 기술들을 사용하여 유한한 가능성으로 줄인다.1차 논리의 해결규칙은 [math(\forall)]만 사용된 특별한 CNF인 PCNF(prenex conjunctive normal form, 이하 PCNF)에서만 적용된다. 그렇기 때문에 Skolemization을 사용해야한다. 이 Skolemization의 아이디어는 [math(\forall x, \exists y, R(x,y))]를 [math(\forall x, R(f(x),x) )]로 바꾸어서 생각하는 것이다. 이 Skolemization을 이용하여 PCNF로 바꾸면 이제 두 가지 해결규칙을 쓸 수 있다.
4.2.1. 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차 논리의 모델을 이용하여 증명한다.
4.2.2. ground resolution
Ground resolution은 두 ground term에 대해서 진행하는 해결 규칙이다. ground term이란 자유 변수(free variable)이 포함되지 않은 term을 말하는데 즉, 함수(function), 관계(relation), 그리고 상수(constant)[4]로만 이루어 진 것이다. ground resolution은 0차 논리의 propositional resolution과 거의 동일하다.4.2.3. General resolution
General resolution은 ground term이 아닌 자유 변수를 포함한 term들에 대한 해결규칙이다. 이 general resolution의 핵심 아이디어는 단일화(unification)이다. most general unfier를 이용하여 두 절(clause)을 충동(clash)시켜 해결규칙을 적용한다.[math( \displaystyle { \Gamma \vdash \forall x \left( A \lor C_1 \right) \quad \Gamma \vdash \forall y \left( B \lor C_2 \right) \over \Gamma \vdash A \left[ \sigma \right] \lor B \left[ \sigma \right] } \quad \sigma \text{ is a most general unfier of } C_1 \text{ and } C_2 )]
이 규칙에 따라 진행할 경우 0차 논리와 같이 마지막에 [math( A \land \neg A )]의 형태가 나오는데 이를 통해 모순을 유도하여 귀류법으로 명제를 증명한다.
5. 현재
자동정리증명은 계속 연구되어 오는 분야다. 하지만 워낙 비효율적이고 조금만 복잡해져도 시간이 오래걸리기에 간단하지만 수학자가 증명하기 귀찮은 잡다한 따름정리나 보조정리 정도의 증명을 돕는다. 이를 통해 수학자가 증명할 때 잡다한 귀찮은 일을 줄여주는 역할에 그치고 있다. 원래 NP문제는 일차 근사 알고리즘 (first approximate algorithm)이 존재해 이를 사용하지만 최근에는 머신러닝을 도입하자는 목소리가 나와 머신러닝을 도입하는 추세다. 실제 인간 수학자가 증명하는 방식을 생각해보면 어쩌면 머신러닝이 더 합당한 조치일 수도 있다. 머신러닝은 현재 경험적 알고리즘(heuristic algorithm)을 고르는데 쓰이고 있다. 예시로 E-prover라는 ATP는 대략 80개의 경험적 알고리즘을 가지고 있다고 한다.[1] 예시로 연속체 가설이 있다.[2] 튜링기계(Turing machine)가 올바른 표현이나 이해를 돕기 위하여 컴퓨터로 서술하였다[3] 귀류법을 사용한다는 시점에서 증명시스템(proof system)은 자연연역(natural deduction)을 사용하는 것을 전제로 한다는 것을 알 수 있다.[4] 원래 constant는 파라미터의 개수(arity)가 0인 함수로 정의하지만 직관적 이해를 돕기 위해 구분하여 적었다.