증명 보조기: 두 판 사이의 차이
내용 삭제됨 내용 추가됨
"Proof assistant" 문서를 번역하여 만듦 |
(차이 없음)
|
2022년 4월 11일 (월) 00:18 판
컴퓨터 과학 및 수리 논리학에서 증명 보조기 또는 대화형 정리 증명기는 인간-기계 협업에 의한 형식 증명을 보조하는 소프트웨어 도구이다. 증명 보조기는 대화형 증명 편집기 또는 기타 인터페이스가 포함하며, 이를 통해 인간의 증명 검색을 돕는다. 또한 증명 보조기는 증명의 세부 정보를 컴퓨터에 저장하고, 증명의 일부 단계를 컴퓨터로 계산한다.
시스템 비교
이름 | 마지막 버전 | 개발자 | 구현 언어 | 기능 | |||||
---|---|---|---|---|---|---|---|---|---|
고차 논리 | Dependent types | Small kernel | 자동 정리 증명 | Proof by reflection | Code generation | ||||
ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | Common Lisp | 아니요 | Untyped | 아니요 | 예 | 예[1] | Already executable |
Agda | 2.6.2 | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg) | Haskell | 예 | 예 | 예 | 아니요 | 부분적 | Already executable |
Albatross | 0.4 | Helmut Brandl | OCaml | 예 | 아니요 | 예 | 예 | 알 수 없음 | 아직 아님 Implemented |
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 | Standard ML | 예 | 아니요 | 예 | 예 | 아니요 | 예 |
Idris | 2 0.4.0. | Edwin Brady | Idris | 예 | 예 | 예 | 알 수 없음 | 부분적 | 예 |
Isabelle | Isabelle2021 (February 2021) | Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel | Standard ML, Scala | 예 | 아니요 | 예 | 예 | 예 | 예 |
Lean | v3.4.2 (official release)[3] v3.39.1 (community release)[4] v4.0.0-m3 (pre-release)[5] | Microsoft Research | C++ | 예 | 예 | 예 | 예 | 예 | 알 수 없음 |
LEGO (not affiliated with Lego) | 1.3.1 | Randy Pollack (Edinburgh) | Standard ML | 예 | 예 | 예 | 아니요 | 아니요 | 아니요 |
Mizar | 8.1.05 | Białystok University | Free Pascal | 부분적 | 예 | 아니요 | 아니요 | 아니요 | 아니요 |
NuPRL | 5 | Cornell University | Common Lisp | 예 | 예 | 예 | 예 | 알 수 없음 | 예 |
PVS | 6.0 | SRI International | Common Lisp | 예 | 예 | 아니요 | 예 | 아니요 | 알 수 없음 |
Twelf | 1.7.1 | Frank Pfenning and Carsten Schürmann | Standard ML | 예 | 예 | 알 수 없음 | 아니요 | 아니요 | 알 수 없음 |
- ACL2 – Boyer-Moore 전통의 프로그래밍 언어, 1차 논리 이론 및 정리 증명자(대화형 모드와 자동 모드 모두 포함).
- Coq - 수학적 주장의 표현을 허용하고, 이러한 주장의 증명을 기계적으로 확인하고, 형식적 증명을 찾는 데 도움을 주고, 형식 사양의 구성적 증명에서 인증된 프로그램을 추출합니다.
- HOL 정리 증명자 – 궁극적으로 LCF 정리 증명자 에서 파생된 도구 제품군입니다. 이러한 시스템에서 논리적 핵심은 프로그래밍 언어의 라이브러리입니다. 정리는 언어의 새로운 요소를 나타내며 논리적 정확성을 보장하는 "전략"을 통해서만 도입될 수 있습니다. 전략 구성을 통해 사용자는 시스템과의 상호 작용이 비교적 적은 중요한 증거를 생성할 수 있습니다. 가족 구성원은 다음과 같습니다.
- HOL4 – 아직 활발히 개발 중인 "기본 자손". 모스크바 ML 및 Poly/ML 모두 지원 . BSD 스타일 라이센스가 있습니다.
- HOL Light – 번성하는 "미니멀리스트 포크". OCaml 기반.
- ProofPower – 독점이 된 다음 오픈 소스로 돌아 왔습니다. 표준 ML을 기반으로 합니다.
- IMPS, 대화형 수학 증명 시스템 [6]
- Isabelle은 HOL의 후속인 대화식 정리 증명자이다. 주요 코드 기반은 BSD 라이선스이지만 Isabelle 배포판은 다른 라이선스를 가진 많은 애드온 도구를 번들로 제공한다.
- Jape – 자바 기반.
- Lean
- LEGO
- Matita – 귀납적 구성의 미적분에 기반한 조명 시스템.
- MINLOG – 1차 최소 논리를 기반으로 하는 증명 보조기.
- Mizar – 자연 연역 스타일의 1차 논리와 타르스키-그로텐디크 집합론 을 기반으로 하는 증명 보조기.
- PhoX – 확장 가능한 고차 논리에 기반한 증명 보조기.
- 프로토타입 검증 시스템 (PVS) – 고차 논리에 기반한 증명 언어 및 시스템.
- TPS 및 ETPS – 단순 형식 람다 대수의 독립적인 공식화와 구현을 기반으로 하는 대화형 증명 보조기.
- Typelab
- Yarrow
정리 증명기 박물관은 중요한 문화/과학적 인공물인 정리 증명 시스템의 향후 분석을 위해 소스를 보존하기 위한 이니셔티브이다. 위에서 언급한 많은 시스템의 소스가 여기에 있다.
사용자 인터페이스
증명 보조기를 위한 인기 있는 프론트엔드는 에든버러 대학교에서 개발된 Emacs 기반 Proof General이다. Coq에는 OCaml/GTK 를 기반으로 하는 CoqIDE가 포함되어 있다. Isabelle에는 jEdit 및 문서 지향 증명 처리를 위한 Isabelle/Scala 인프라를 기반으로 하는 Isabelle/jEdit가 포함되어 있다. Coq, Isabelle의 비주얼 스튜디오 코드 확장도 개발되었다. [7]
같이 보기
- 자동 정리 증명
- 컴퓨터를 이용한 증명
- QED 선언문
- 형식 검증
- 만족도 모듈로 이론
- Metamath – 이 언어에 대한 증명 검사기 및 수천 개의 입증된 정리 데이터베이스와 함께 공식화된 수학을 개발하기 위한 언어.
노트
참고문헌
- Henk Barendregt and Herman Geuvers (2001). "Proof-assistants using Dependent Type Systems". In Handbook of Automated Reasoning.
- Frank Pfenning (2001). "Logical frameworks". In Handbook of Automated Reasoning.
- Frank Pfenning (1996). "The Practice of Logical Frameworks".
- Robert L. Constable (1998). "Types in computer science, philosophy and logic". In Handbook of Proof Theory.
- H. Geuvers. "Proof assistants: History, ideas and future".
- Freek Wiedijk. "The Seventeen Provers of the World"
외부 링크
- 종속 유형이 있는 인증된 프로그래밍 의 "소개" .
- Coq Proof Assistant 소개 (대화형 정리 증명에 대한 일반적인 소개 포함)
- Agda 사용자를 위한 대화식 정리 증명
- 정리 증명 도구 목록
- 카탈로그
- 범주별 디지털 수학: Tactic Provers
- 자동 연역 체계 및 그룹
- 정리 증명 및 자동 추론 시스템
- 기존의 기계화 추론 시스템 데이터베이스
- NuPRL: 기타 시스템
- 특정 논리적 프레임워크 및 구현
- DMOZ : 과학: 수학: 논리 및 기초: 계산 논리: 논리 프레임워크
[[분류:Category:수학]] [[분류:논리학]] [[분류:Category:컴퓨터 과학]] [[분류:Category:증명 보조기]]
- ↑ Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). 〈Meta Reasoning in ACL2〉 (PDF). 《Theorem Proving in Higher Order Logics》. Lecture Notes in Computer Science 3603. 163–178쪽. doi:10.1007/11541868_11. ISBN 978-3-540-28372-0.
- ↑ Search for "proofs by reflection": arXiv:1803.06547
- ↑ “Lean Theorem Prover Releases page”. 《GitHub》.
- ↑ “Lean Community Releases Page”. 《GitHub》.
- ↑ “Lean 4 Releases Page”. 《GitHub》.
- ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). “IMPS: An interactive mathematical proof system”. 《Journal of Automated Reasoning》 11 (2): 213–248. doi:10.1007/BF00881906. 2020년 1월 22일에 확인함.
- ↑ Wenzel, Makarius. “Isabelle”. 2019년 11월 2일에 확인함.