자동화된 추론

3. 주요 기여

알프레드 노스 화이트헤드와 버트런드 러셀의 수학 원리(Principia Mathematica)는 수리 논리학 발전에 큰 영향을 미친 기념비적인 저서이다. 이 책은 모든 수학적 명제를 기호 논리학으로 표현하고 증명하는 것을 목표로 하였으며, 1910년, 1912년, 1913년에 걸쳐 세 권으로 출판되었다.^[6]

1956년에는 앨런 뉴얼, 클리프 쇼, 허버트 A. 사이먼이 논리 이론가(Logic Theorist)라는 초기 인공지능 프로그램을 개발했다. 이 프로그램은 인간의 문제 해결 방식을 모방하여 수학 원리에 나오는 정리들을 증명하도록 설계되었으며, 실제로 52개의 정리 중 38개를 증명하는 데 성공했다.^[7] 특히, 논리 이론가는 기존 증명보다 더 간결하고 효율적인 증명을 발견하기도 했다.

이후 자동화된 추론은 다양한 분야에서 발전을 거듭하여, 여러 수학 난제를 해결하는 데 기여했다. (하위 섹션 '형식적 증명의 예'에서 상세한 표를 제공하므로, 여기서는 생략한다.)

3. 1. 수학 원리 (Principia Mathematica)

3. 2. 논리 이론가 (Logic Theorist)

3. 3. 형식적 증명의 예

4. 주요 증명 시스템

자동 추론에 사용되는 대표적인 증명 시스템은 다음과 같다.

• 보이어-무어 정리 증명기 (NQTHM): 존 매카시와 우디 블레드소의 영향을 받아 설계되었으며, 리습으로 구축된 완전 자동 정리 증명기이다.
• HOL Light: OCaml로 작성되었으며, 단순하고 명확한 논리적 기반을 갖도록 설계되었다.
• Coq: 프랑스에서 개발된 증명 보조기로, 명세로부터 실행 가능한 프로그램을 자동 추출할 수 있다.

4. 1. 보이어-무어 정리 증명기 (Nqthm)

• 리습을 작업 논리로 사용
• 전체 재귀 함수에 대한 정의 원칙에 의존
• 재작성 및 "기호적 평가"의 광범위한 사용
• 기호적 평가 실패를 기반으로 하는 귀납적 휴리스틱^[13][14]

4. 2. HOL Light

4. 3. Coq

5. 응용

자동 추론은 자동 정리 증명기 구축에 크게 응용된다. 로직 시어리스트(Logic Theorist)와 같이 정리를 새롭게 증명하는 방법을 제시하기도 한다.^[27] 자동 추론 프로그램은 논리학, 수학, 컴퓨터 과학, 논리 프로그래밍, 소프트웨어 및 하드웨어 설계 검증, 회로 설계 등 다양한 분야의 문제를 해결하는 데 사용되고 있다.^[27] TPTP는 이러한 문제들을 모아 놓은 라이브러리이며, 정기적으로 업데이트된다. 또한, CADE라는 학회에서 정기적으로 자동 정리 증명기 경진대회가 개최되고 있으며, 경진대회 문제는 TPTP 라이브러리에서 선택된다.^[27]

5. 1. 자동 정리 증명

5. 2. 기타 응용 분야

6. 관련 학회 및 학술지

자동추론학회(Association for Automated Reasoning, AAR)는 자동 추론 저널을 발간한다.

6. 1. 학회

• 자동 추론 국제 합동 학술대회(IJCAR)
• 자동 증명 학술대회(CADE)
• 해석표와 관련 방법을 이용한 자동 추론 국제 학술대회(TABLEAUX)
• 국제 자동 추론 학술대회 (IJCAR)
• 자동 증명 학술대회 (CADE)
• 해석표와 관련 방법을 이용한 자동 추론 국제 학술대회 (TABLEAUX)
• 논리 구현 국제 워크숍
• 자동 추론에서 경험적으로 성공적인 주제에 관한 워크숍 시리즈

6. 2. 학술지

• Journal of Automated Reasoning

6. 3. 관련 단체

• 자동 추론 협회 (AAR)는 자동추론학회(Association for Automated Reasoning, AAR)에서 발간하는 학회지이다.
• Journal of Automated Reasoning

참조

_[1] 논문 Analogy and abduction in automated deduction http://citeseerx.ist[...]
_[2] 인용 필요 2023-05-00
_[3] 웹사이트 Formal Proof https://www.ams.org/[...] University of Pittsburgh 2010-10-19
_[4] 웹사이트 Automated Deduction (AD) http://www.cs.cornel[...] 2010-10-19
_[5] 서적 The Prehistory and Early History of Automated Deduction https://www.springer[...] Springer
_[6] 웹사이트 Principia Mathematica http://plato.stanfor[...] 2010-10-19
_[7] 웹사이트 The Logic Theorist and its Children http://www.cs.swarth[...] 2010-10-18
_[8] 웹사이트 Little Engines of Proof http://www.csl.sri.c[...] Computer Science Laboratory, SRI International 2010-10-19
_[9] 서적 Metamathematics, Machines, and Gödel's Proof https://books.google[...] Cambridge University Press
_[10] 논문 A Mechanical Proof of Quadratic Reciprocity
_[11] 논문 A Machine-Checked Proof of the Odd Order Theorem http://www.cs.unibo.[...]
_[12] 논문 Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
_[13] 웹사이트 The Boyer-Moore Theorem Prover http://www.cs.utexas[...] 2010-10-23
_[14] 웹사이트 The PLTP Archive https://www.cs.utexa[...] 2023-07-27
_[15] 웹사이트 HOL Light: an overview http://www.cl.cam.ac[...] 2010-10-23
_[16] 웹사이트 Introduction to Coq http://coq.inria.fr/[...] 2010-10-23
_[17] 웹사이트 Automated Reasoning http://plato.stanfor[...] 2010-10-10
_[18] 웹사이트 Formal Proof http://www.ams.org/n[...] University of Pittsburgh 2010-10-19
_[19] 웹사이트 Automated Deduction (AD) http://www.cs.cornel[...] 2010-10-19
_[20] 서적 The Prehistory and Early History of Automated Deduction
_[21] 웹사이트 Principia Mathematica http://plato.stanfor[...] Stanford University 2010-10-19
_[22] 웹사이트 The Logic Theorist and its Children http://www.cs.swarth[...] 2010-10-18
_[23] 웹사이트 Little Engines of Proof http://www.csl.sri.c[...] Computer Science Laboratory, SRI International 2010-10-19
_[24] 웹사이트 The Boyer-Moore Theorem Prover http://www.cs.utexas[...] 2010-10-23
_[25] 웹사이트 HOL Light: an overview http://www.cl.cam.ac[...] 2010-10-23
_[26] 웹사이트 Introduction to Coq http://coq.inria.fr/[...] 2010-10-23
_[27] 웹사이트 Automated Reasoning http://plato.stanfor[...] Stanford Encyclopedia 2010-10-10
_[28] 인물