증명 보조기
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
1. 개요
증명 보조기는 수학적 주장의 표현, 증명 검증, 형식적 증명 탐색을 돕는 도구이다. 주요 증명 보조기에는 ACL2, Agda, Coq, HOL 정리 증명기, Isabelle, Lean 등이 있으며, 각기 다른 특징과 기능을 제공한다. 이러한 시스템은 고차 논리, 종속 유형, 자동 정리 증명, 코드 생성과 같은 기능을 지원하며, 다양한 프로그래밍 언어로 구현된다. 사용자 인터페이스는 Emacs 기반의 Proof General, CoqIDE, Isabelle/jEdit 등이 있으며, 비주얼 스튜디오 코드 확장도 개발되었다.
다양한 증명 보조기 시스템들을 비교하면 다음과 같다. 각 시스템의 특징, 기능, 개발 언어 등은 아래 표와 같이 정리할 수 있다.
2. 시스템 비교
이름 마지막 버전 개발자 구현 언어 기능 고차 논리 Dependent types Small kernel 자동 정리 증명 Proof by reflection Code generation ACL2 8.3 Matt Kaufmann and J Strother Moore 커먼 리스프 예 예[1] 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* 예 예 예 예[2] 예 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)[3] v3.39.1 (community release)[4] v4.0.0-m3 (pre-release)[5] 마이크로소프트 리서치 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[6], 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 | 커먼 리스프 | 예 | 예[1] | ||||
| 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* | 예 | 예 | 예 | 예[2] | 예 | |
| 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)[3] v3.39.1 (community release)[4] v4.0.0-m3 (pre-release)[5] | 마이크로소프트 리서치 | 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[6], Jape, Matita, MINLOG, PhoX, TPS 및 ETPS, Typelab, Yarrow 등의 증명 보조기들이 있다.
[https://theoremprover-museum.github.io/ 정리 증명기 박물관]은 중요한 문화/과학적 인공물인 정리 증명 시스템의 향후 분석을 위해 소스를 보존하기 위한 이니셔티브이며, 위에 언급된 많은 시스템의 소스가 여기에 있다.
2. 1. 1. ACL2
ACL2는 Boyer-Moore 전통을 따르는 프로그래밍 언어이자, 1차 논리 이론 및 정리 증명기이다. ACL2는 대화형 모드와 자동 모드를 모두 지원한다.[1]| 이름 | 마지막 버전 | 개발자 | 구현 언어 | 고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation |
|---|---|---|---|---|---|---|---|---|---|
| ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | 커먼 리스프 | 예 | 예[1] |
2. 1. 2. Coq
Coq는 수학적 주장을 표현하고, 이러한 주장의 증명을 기계적으로 확인하며, 형식적 증명을 찾는 데 도움을 주고, 형식 사양의 구성적 증명에서 인증된 프로그램을 추출하는 기능을 제공한다.[1] Coq는 INRIA에서 개발되었으며, OCaml로 구현되었다. Coq는 고차 논리, 종속 타입(Dependent types), 소형 커널(Small kernel), 자동 정리 증명, 반사에 의한 증명(Proof by reflection), 코드 생성(Code generation) 기능을 모두 지원한다.[1]
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 배포판에는 다른 라이선스를 가진 다양한 애드온 도구들이 포함되어 있다.| 이름 | 마지막 버전 | 개발자 | 구현 언어 | 고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation |
|---|---|---|---|---|---|---|---|---|---|
| Isabelle | Isabelle2021 (February 2021) | Larry Paulson (케임브리지 대학교), Tobias Nipkow (뮌헨 공과대학교) and Makarius Wenzel | 표준 ML, Scala | 예 | 예 | 예 | 예 | 예 |
2. 1. 5. Lean
마이크로소프트 리서치에서 개발한 Lean은 C++로 구현되었다.[3] [4] [5] 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 | 커먼 리스프 | 예 | 예[1] | |||||
| 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* | 예 | 예 | 예 | 예[2] | 예 | ||
| 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 정리 증명기: 궁극적으로 LCF 정리 증명기에서 파생된 도구 제품군이다.
- [http://hol.sourceforge.net/ HOL4]: 아직 활발히 개발 중인 "기본 자손"이다. 모스크바 ML 및 Poly/ML 모두 지원하며, BSD 스타일 라이센스가 있다.
- HOL Light: "미니멀리스트 포크"이다. OCaml 기반이다.
- ProofPower: 독점이 된 다음 오픈 소스로 돌아 왔다. 표준 ML을 기반으로 한다.
- IMPS, 대화형 수학 증명 시스템[6]
- 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]도 개발되었다.[7]
4. 관련 자료
참조
[1]
서적
Theorem Proving in Higher Order Logics
[2]
ArXiv
proofs by reflection
[3]
웹인용
Lean Theorem Prover Releases page
https://github.com/l[...]
[4]
웹인용
Lean Community Releases Page
https://github.com/l[...]
[5]
웹인용
Lean 4 Releases Page
https://github.com/l[...]
[6]
저널
IMPS: An interactive mathematical proof system
https://core.ac.uk/d[...]
1993
[7]
웹인용
Isabelle
https://marketplace.[...]
2019-11-02
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com