증명 보조기
1. 개요
증명 보조기는 수학적 주장의 표현, 증명 검증, 형식적 증명 탐색을 돕는 도구이다. 주요 증명 보조기에는 ACL2, Agda, Coq, HOL 정리 증명기, Isabelle, Lean 등이 있으며, 각기 다른 특징과 기능을 제공한다. 이러한 시스템은 고차 논리, 종속 유형, 자동 정리 증명, 코드 생성과 같은 기능을 지원하며, 다양한 프로그래밍 언어로 구현된다. 사용자 인터페이스는 Emacs 기반의 Proof General, CoqIDE, Isabelle/jEdit 등이 있으며, 비주얼 스튜디오 코드 확장도 개발되었다.
-
컴퓨터 과학 -
수학적 최적화
수학적 최적화는 주어진 집합에서 실수 또는 정수 변수를 갖는 함수의 최댓값이나 최솟값을 찾는 문제로, 변수 종류, 제약 조건, 목적 함수 개수에 따라 다양한 분야로 나뉘며 여러 학문 분야에서 활용된다. -
컴퓨터 과학 -
국제 정보 올림피아드
-
컴퓨터 과학 내 논리 -
자동화된 추론
자동화된 추론은 컴퓨터 프로그램을 사용하여 논리적 추론을 수행하는 인공지능 분야로, 수리 논리학의 발전과 초기 연구를 통해 자동 정리 증명 분야의 기틀을 마련했으며, AI 겨울을 겪었지만 소프트웨어 검증 등 다양한 분야에 활용되며 Coq, HOL Light 등의 증명 보조기가 개발되어 난제들의 형식적 증명에 기여했다. -
컴퓨터 과학 내 논리 -
혼 절
혼 절은 하나의 긍정 리터럴만을 포함하는 분리절이며, 논리 프로그래밍, 자동 정리 증명, 데이터베이스 이론 등 여러 분야에 응용된다. -
논리학 -
모순
모순은 논리학, 철학, 과학 등 다양한 분야에서 사용되는 개념으로, 서로 상반되는 두 가지 주장이나 사실이 동시에 존재하는 상태를 의미하며, 특히 헤겔과 마르크스의 변증법적 유물론에서 사물의 내재적 대립으로서 역사 발전의 원동력으로 간주된다. -
논리학 -
특수
특수는 철학에서는 개별적이고 구체적인 존재를, 언어학에서는 눈에 띄는 또는 예외적인 의미를 가지며, 사회적으로 특별함이 중요하게 여겨지기도 한다.
2. 시스템 비교
다양한 증명 보조기 시스템들을 비교하면 다음과 같다. 각 시스템의 특징, 기능, 개발 언어 등은 아래 표와 같이 정리할 수 있다.
| 이름 | 마지막 버전 | 개발자 | 구현 언어 | 기능 | |||||
|---|---|---|---|---|---|---|---|---|---|
| 고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation | ||||
| ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | 커먼 리스프 | 예 | 예 | ||||
| Agda | 2.6.2 | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg) | 하스켈 | 예 | 예 | 예 | 부분적 | ||
| Albatross | 0.4 | Helmut Brandl | OCaml | 예 | 예 | 예 | 알 수 없음 | ||
| Coq | 8.13.2 | INRIA | OCaml | 예 | 예 | 예 | 예 | 예 | 예 |
| F* | repository | Microsoft Research and INRIA | F* | 예 | 예 | 예 | 예 | 예 | |
| HOL Light | repository | John Harrison | OCaml | 예 | 예 | 예 | |||
| HOL4 | Kananaskis-13 (or repo) | Michael Norrish, Konrad Slind, and others | 표준 ML | 예 | 예 | 예 | 예 | ||
| Idris | 2 0.4.0. | Edwin Brady | Idris | 예 | 예 | 예 | 알 수 없음 | 부분적 | 예 |
| Isabelle | Isabelle2021 (February 2021) | Larry Paulson (케임브리지 대학교), Tobias Nipkow (뮌헨 공과대학교) and Makarius Wenzel | 표준 ML, Scala | 예 | 예 | 예 | 예 | 예 | |
| Lean | v3.4.2 (official release) v3.39.1 (community release) v4.0.0-m3 (pre-release) | 마이크로소프트 리서치 | C++ | 예 | 예 | 예 | 예 | 예 | 알 수 없음 |
| [http://www.dcs.ed.ac.uk/home/lego/ LEGO] (레고와 관련 없음) | 1.3.1 | Randy Pollack (Edinburgh) | 표준 ML | 예 | 예 | 예 | |||
| Mizar | 8.1.05 | 비아위스토크 대학 | Free Pascal | 부분적 | 예 | ||||
| NuPRL | 5 | 코넬 대학교 | 커먼 리스프 | 예 | 예 | 예 | 예 | 알 수 없음 | 예 |
| PVS | 6.0 | SRI International | 커먼 리스프 | 예 | 예 | 예 | 알 수 없음 | ||
| Twelf | 1.7.1 | Frank Pfenning and Carsten Schürmann | 표준 ML | 예 | 예 | 알 수 없음 | 알 수 없음 | ||
이 외에도 IMPS, Jape, Matita, MINLOG, PhoX, TPS 및 ETPS, Typelab, Yarrow 등의 증명 보조기들이 있다.
[https://theoremprover-museum.github.io/ 정리 증명기 박물관]은 중요한 문화/과학적 인공물인 정리 증명 시스템의 향후 분석을 위해 소스를 보존하기 위한 이니셔티브이며, 위에 언급된 많은 시스템의 소스가 여기에 있다.
2.1. 주요 증명 보조기
다음은 주요 증명 보조기들에 대한 표이다.
| 이름 | 마지막 버전 | 개발자 | 구현 언어 | 기능 | |||||
|---|---|---|---|---|---|---|---|---|---|
| 고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation | ||||
| ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | 커먼 리스프 | 예 | 예 | ||||
| Agda | 2.6.2 | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg) | 하스켈 | 예 | 예 | 예 | 부분적 | ||
| Albatross | 0.4 | Helmut Brandl | OCaml | 예 | 예 | 예 | 알 수 없음 | ||
| Coq | 8.13.2 | INRIA | OCaml | 예 | 예 | 예 | 예 | 예 | 예 |
| F* | repository | Microsoft Research and INRIA | F* | 예 | 예 | 예 | 예 | 예 | |
| HOL Light | repository | John Harrison | OCaml | 예 | 예 | 예 | |||
| HOL4 | Kananaskis-13 (or repo) | Michael Norrish, Konrad Slind, and others | 표준 ML | 예 | 예 | 예 | 예 | ||
| Idris | 2 0.4.0. | Edwin Brady | Idris | 예 | 예 | 예 | 알 수 없음 | 부분적 | 예 |
| Isabelle | Isabelle2021 (February 2021) | Larry Paulson (케임브리지 대학교), Tobias Nipkow (뮌헨 공과대학교) and Makarius Wenzel | 표준 ML, Scala | 예 | 예 | 예 | 예 | 예 | |
| Lean | v3.4.2 (official release) v3.39.1 (community release) v4.0.0-m3 (pre-release) | 마이크로소프트 리서치 | C++ | 예 | 예 | 예 | 예 | 예 | 알 수 없음 |
| LEGO (레고와 관련 없음) | 1.3.1 | Randy Pollack (Edinburgh) | 표준 ML | 예 | 예 | 예 | |||
| Mizar | 8.1.05 | 비아위스토크 대학 | Free Pascal | 부분적 | 예 | ||||
| NuPRL | 5 | 코넬 대학교 | 커먼 리스프 | 예 | 예 | 예 | 예 | 알 수 없음 | 예 |
| PVS | 6.0 | SRI International | 커먼 리스프 | 예 | 예 | 예 | 알 수 없음 | ||
| Twelf | 1.7.1 | Frank Pfenning and Carsten Schürmann | 표준 ML | 예 | 예 | 알 수 없음 | 알 수 없음 | ||
이 외에도 IMPS, Jape, Matita, MINLOG, PhoX, TPS 및 ETPS, Typelab, Yarrow 등의 증명 보조기들이 있다.
[https://theoremprover-museum.github.io/ 정리 증명기 박물관]은 중요한 문화/과학적 인공물인 정리 증명 시스템의 향후 분석을 위해 소스를 보존하기 위한 이니셔티브이며, 위에 언급된 많은 시스템의 소스가 여기에 있다.
2.1.1. ACL2
ACL2는 Boyer-Moore 전통을 따르는 프로그래밍 언어이자, 1차 논리 이론 및 정리 증명기이다. ACL2는 대화형 모드와 자동 모드를 모두 지원한다.
2.1.2. Coq
Coq는 수학적 주장을 표현하고, 이러한 주장의 증명을 기계적으로 확인하며, 형식적 증명을 찾는 데 도움을 주고, 형식 사양의 구성적 증명에서 인증된 프로그램을 추출하는 기능을 제공한다. Coq는 INRIA에서 개발되었으며, OCaml로 구현되었다. Coq는 고차 논리, 종속 타입(Dependent types), 소형 커널(Small kernel), 자동 정리 증명, 반사에 의한 증명(Proof by reflection), 코드 생성(Code generation) 기능을 모두 지원한다.
2.1.3. HOL 정리 증명기
HOL 정리 증명기는 LCF 정리 증명기에서 파생된 도구 제품군이다. 이러한 시스템에서 논리적 핵심은 프로그래밍 언어의 라이브러리이며, 정리는 언어의 새로운 요소를 나타낸다. 논리적 정확성을 보장하는 "전략(strategy)"을 통해서만 정리가 도입될 수 있으며, 전략 구성을 통해 사용자는 시스템과의 상호 작용을 비교적 적게 하면서도 중요한 증명을 생성할 수 있다. 다음은 HOL 정리 증명기에 포함된 증명 보조기들이다.
| 이름 | 설명 |
|---|---|
| HOL4 | 모스크바 ML 및 Poly/ML을 모두 지원하는, 아직 활발히 개발 중인 "기본 자손"이다. BSD 스타일 라이센스를 따른다. |
| HOL Light | OCaml 기반의 "미니멀리스트 포크"이다. |
| ProofPower | 표준 ML을 기반으로 하며, 독점되었다가 오픈 소스로 돌아왔다. |
2.1.4. Isabelle
케임브리지 대학교의 Larry Paulson, 뮌헨 공과대학교의 Tobias Nipkow, Makarius Wenzel이 개발한 대화형 정리 증명기이다. 표준 ML과 Scala로 구현되었다. 고차 논리(HOL)의 후속이며, 주요 코드 기반은 BSD 라이선스를 따르지만, Isabelle 배포판에는 다른 라이선스를 가진 다양한 애드온 도구들이 포함되어 있다.
2.1.5. Lean
마이크로소프트 리서치에서 개발한 Lean은 C++로 구현되었다. Lean은 고차 논리, Dependent types, Small kernel, 자동 정리 증명, Proof by reflection, Code generation 등의 기능을 지원한다.
2.2. 기타 증명 보조기
다음은 기타 증명 보조기 시스템에 대한 간략한 정보이다.
| 이름 | 개발자 | 구현 언어 | 고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation | |
|---|---|---|---|---|---|---|---|---|---|
| ACL2 | Matt Kaufmann and J Strother Moore | 커먼 리스프 | 예 | 예 | |||||
| Agda | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg) | 하스켈 | 예 | 예 | 예 | 부분적 | |||
| Albatross | Helmut Brandl | OCaml | 예 | 예 | 예 | 알 수 없음 | |||
| Coq | INRIA | OCaml | 예 | 예 | 예 | 예 | 예 | 예 | |
| F* | Microsoft Research and INRIA | F* | 예 | 예 | 예 | 예 | 예 | ||
| HOL Light | John Harrison | OCaml | 예 | 예 | 예 | ||||
| HOL4 | Michael Norrish, Konrad Slind, and others | 표준 ML | 예 | 예 | 예 | 예 | |||
| Idris | Edwin Brady | Idris | 예 | 예 | 예 | 알 수 없음 | 부분적 | 예 | |
| Isabelle | Larry Paulson (케임브리지 대학교), Tobias Nipkow (뮌헨 공과대학교) and Makarius Wenzel | 표준 ML, Scala | 예 | 예 | 예 | 예 | 예 | ||
| Lean | 마이크로소프트 리서치 | C++ | 예 | 예 | 예 | 예 | 예 | 알 수 없음 | |
| [http://www.dcs.ed.ac.uk/home/lego/ LEGO] (레고와 관련 없음) | Randy Pollack (Edinburgh) | 표준 ML | 예 | 예 | 예 | ||||
| Mizar | 비아위스토크 대학 | Free Pascal | 부분적 | 예 | |||||
| NuPRL | 코넬 대학교 | 커먼 리스프 | 예 | 예 | 예 | 예 | 알 수 없음 | 예 | |
| PVS | SRI International | 커먼 리스프 | 예 | 예 | 예 | 알 수 없음 | |||
| Twelf | Frank Pfenning and Carsten Schürmann | 표준 ML | 예 | 예 | 알 수 없음 | 알 수 없음 |
* [[ACL2]]: Boyer-Moore 전통의 프로그래밍 언어, 1차 논리 이론 및 정리 증명기(대화형 모드와 자동 모드 모두 포함)이다.
* [[Coq]]: 수학적 주장의 표현을 허용하고, 이러한 주장의 증명을 기계적으로 확인하며, 형식적 증명을 찾는 데 도움을 주고, 형식 사양의 구성적 증명에서 인증된 프로그램을 추출한다.
* [[HOL 정리 증명자|HOL 정리 증명기]]: 궁극적으로 LCF 정리 증명기에서 파생된 도구 제품군이다.
* [http://hol.sourceforge.net/ HOL4]: 아직 활발히 개발 중인 "기본 자손"이다. 모스크바 ML 및 Poly/ML 모두 지원하며, BSD 스타일 라이센스가 있다.
* [[홀 라이트|HOL Light]]: "미니멀리스트 포크"이다. OCaml 기반이다.
* [[프루프파워|ProofPower]]: 독점이 된 다음 오픈 소스로 돌아 왔다. 표준 ML을 기반으로 한다.
* IMPS, 대화형 수학 증명 시스템
* [[이사벨 정리 증명자|Isabelle]]: HOL의 후속인 대화식 정리 증명자이다. 주요 코드 기반은 BSD 라이선스이지만 Isabelle 배포판은 다른 라이선스를 가진 많은 애드온 도구를 번들로 제공한다.
* [[제이프(소프트웨어)|Jape]]: 자바 기반이다.
* [[린(증명 조수)|Lean]]
* [http://www.dcs.ed.ac.uk/home/lego/ LEGO]
* [[마티타|Matita]]: 귀납적 구성의 미적분에 기반한 조명 시스템이다.
* [[밍로그|MINLOG]]: 1차 최소 논리를 기반으로 하는 증명 보조기이다.
* [[미자르 시스템|Mizar]]: 자연 연역 스타일의 1차 논리와 타르스키-그로텐디크 집합론을 기반으로 하는 증명 보조기이다.
* [[팍스|PhoX]]: 확장 가능한 고차 논리에 기반한 증명 보조기이다.
* [[프로토타입 검증 시스템|PVS]]: 고차 논리에 기반한 증명 언어 및 시스템이다.
* [http://gtps.math.cmu.edu/tps.html TPS 및 ETPS]: 단순 형식 람다 대수의 독립적인 공식화와 구현을 기반으로 하는 대화형 증명 보조기이다.
* [http://www.informatik.uni-ulm.de/ki/typelab.html Typelab]
* [https://www.cs.ru.nl/~janz/yarrow/ Yarrow]
[https://theoremprover-museum.github.io/ 정리 증명기 박물관]은 중요한 문화/과학적 인공물인 정리 증명 시스템의 향후 분석을 위해 소스를 보존하기 위한 이니셔티브이다.
3. 사용자 인터페이스
증명 보조기를 위한 인기 있는 프론트엔드는 에든버러 대학교에서 개발된 Emacs 기반 Proof General이다. Coq에는 OCaml/GTK를 기반으로 하는 CoqIDE가 포함되어 있다. Isabelle에는 jEdit 및 문서 지향 증명 처리를 위한 Isabelle/Scala 인프라를 기반으로 하는 Isabelle/jEdit가 포함되어 있다. 비주얼 스튜디오 코드 확장인 [https://marketplace.visualstudio.com/items?itemName=siegebell.vscoq Coq], [https://marketplace.visualstudio.com/items?itemName=makarius.isabelle Isabelle]도 개발되었다.