KSATP 연구회 부스도 많이 오세요

Introduction

자동정리증명은 자동으로 정리(Theorem)를 증명하는 알고리즘에 관한 문제이다. 어떠한 공리와 명제를 입력 받고 증명 시스템을 입력 받으면 증명 시스템을 이용하여 공리로부터 명제를 이끌어 내는 것이다. 이러한 것이 가능한 이유는 공리의 개수가 유한하고(개수가 무한히 많은 공리도 있으나 유한한 공리로 바꿀 수 있을 것이다) 증명 시스템 또한 유한하므로 이들을 잘 조합하면 알고리즘도 증명을 하는 것이 가능하다는 것을 알 수 있을 것이다. 자동정리증명은 세가지 부류로 나눌 수 있는데 일반적인 자동정리증명과 Human-readable, 그리고 Interactive가 있다. 일반적인 자동정리증명은 알고리즘이 자동으로 증명을 해주나 증명 과정을 사람이 보고 이해하는 것이 쉽지 않아 Provable을 판단하는 용도로 제한된다. Human-readable은 사람이 읽을 수 있는 증명 과정을 제공해주는데 이 과정이 복잡하여 효율이 떨어진다. Interactive Theorem Proving은 Proof Assistant라고도 불리는데 사람과 상호작용하여 자잘하고 증명하기 까다로운 Lemma는 자동정리증명이 증명을 해주고 전체적인 증명 흐름은 사람이 짜는 형태이다. 현재 수학 학회에서 널리 사용되는 자동증명검증 프로그램 Coq도 Interactive Theorem Proving이 가능하다.

NP-Completeness

자동정리증명은 유명한 NP-complete 문제 중 하나이다. 이를 확인하기 위해서는 자동정리증명이 NP이고 NP-hard인지 확인해야 하는데, NP-hard임은 SAT으로부터의 환원(reduction)을 쉽게 구성할 수 있으므로 자명하다. NP임을 보이는 방법은 여러가지가 있는데 정의에 입각하여 증명하는 편이 쉽다. 자동정리증명의 검증자(certifier) 알고리즘은 어떠한 정리와 증명을 입력받으면 알맞는 증명인지 확인하는 알고리즘일 것이다. 이 알고리즘은 다항 시간(poly-time)안에 가능함이 이미 증명되었고 Coq라는 유명한 프로그램도 있다. 따라서 자동정리증명은 NP-complete이고 이에 따라 사람들은 보통 자동정리증명의 다항시간 알고리즘을 찾지 않는다.

First Order Logic

First Order Logic(일차 논리)란, quantifier가 variable에만 허용되는 논리로 특정 언어를 지칭하는 것이 아니라 언어들의 성격에 따라 분류한 하나의 집합으로 생각해야 한다. 일차 논리 이외에도 이차 논리, 고차 논리도 있는데 이들은 relation과 function에도 quantifier가 붙는 것을 허용하는 논리다. 또 영차 논리도 있는데 영차 논리는 quantifier가 허용되지 않는 단순한 형태의 언어다. 이 문서에서 서술할 모든 논리학적 성질은 전부 일차 논리에 근거하여 작성할 것이다.

일차 논리인 특정한 언어는 두 가지로 나누어서 생각할 수 있는데 proof system과 syntax다. Syntax는 특정 언어가 다른 일차 논리와 다르게 이 언어에서만 사용되는 기호들을 의미한다. 예를 들어 덧셈의 + 기호는 집합에서 사용되지 않으므로 syntax라고 할 수 있다. 두번째로 proof system는 가장 중요하다고 할 수 있는데 Theory(어떠한 formula로 axiom과 같은 의미다. 이 문서에서는 Theorem과 Theory로 나누어서 사용하겠다.)로부터 Theorem을 이끌어내는 추론 방식이다. 유명한 proof system에는 Hilbert style과 Natural Deduction(Sequent Calculus)등이 있는데 우리가 일반적으로 알고 있는 proof system이 Natural Deduction이므로 이 문서에서는 Natural Deduction을 가정하고 작성하겠다.

이제 일차 논리의 성질들에 대해서 알아보자.
We said $\mathcal{L}$-theory $\mathcal{T}$ is consistent, $Con(\mathcal{T})$, if there is no $A \in \mathcal{L} _ {S}$ s.t. $\mathcal{T} \vdash A$ and $\mathcal{T} \vdash \neg A$.
Also, we said $\mathcal{L}$-theory $\mathcal{T}$ is complete if for $^{\forall} A\ \in \mathcal{L}_{S}$, $\mathcal{T} \vdash A$ or $\mathcal{T} \vdash \neg A$, but not both.

즉 어떤 Theory $\mathcal{T}$가 complete하면 consistent를 만족하는 것이다.
그런데 괴델의 불완전성 정리에 의하면 모든 일차 논리의 Theory는 complete하지 않는다.
즉, 항상 Theory와 independent한, 증명불가능인, Theorem이 존재한다는 것이다.
그래서 일반적으로 자동정리증명 프로그램은 증명 불가능한 명제를 고려하지 않는다.
증명불가능의 예시를 보기 위해 ZFC에 대해 알아보자.

ZFC

ZFC(Zermelo–Fraenkel with axiom of Choice)는 가장 유명한 집합 공리계로 유한한 공리계의 대표 예시라고 할 수 있다. ZFC에는 확장 공리(axiom of extensionality), 정칙성 공리(axiom of regularity), 짝 공리(axiom of pairing), 합집합 공리(axiom of union), 멱집합 공리(axiom of power set), 무한 공리(axiom of infinity), 분류 공리꼴(axiom schema of specification), 치환 공리꼴(axiom schema of replacement), 그리고 선택 공리(axiom of choice)로 이루어져있다. 사실 집합 공리의 경우 간단하게 표현이 가능하지 않을까라고 생각하기 쉽지만 Russel의 패러독스를 보면 생각이 바뀔 것이다. 이렇게 수학자들이 고심하여 열심히 만든 공리계 ZFC조차 증명 불가능한 Theorem들이 있는데 대표적인 예시가 연속체 가설(continuum hypothesis)이다. 이 문제는 자연수 집합의 크기와 실수 집합의 크기 사이의 크기를 가지는 무한 집합이 존재하는 가에 대한 문제로(또는 $2^{\aleph_0}=\aleph_1$으로 이해할 수도 있다.) 증명불가능이 증명되었다.

만약 이 글을 읽고 자동정리증명에 흥미가 생겼다면 이번 SAF의 KSATP 부스에서 더 자세한 설명을 들을 수 있다.