프루프 어시스턴트

Proof assistant
컴퓨터 사이언스의 검증에 대해서는, 정식 검증을 참조해 주세요.
학술회의는 인터랙티브 정리 증명(회의)을 참조해 주세요.
인터랙티브 증명 시스템과 혼동하지 마십시오.
Coq의 대화형 증명 세션IDE: 왼쪽에 프루프 스크립트가 표시되고 오른쪽에 프루프 상태가 표시됩니다.

컴퓨터 과학 및 수리 논리학에서, 증명 보조자 또는 인터랙티브 정리 프로버는 인간과 기계의 협업에 의한 공식 증명 개발을 지원하는 소프트웨어 도구입니다.여기에는 일종의 인터랙티브한 증명 편집기 또는 다른 인터페이스가 포함되며, 이를 통해 인간은 증명, 세부사항 및 컴퓨터에 의해 제공되는 몇 가지 단계에 대한 검색을 안내할 수색을 안내할 수 있습니다.

시스템 비교

다음 항목도 참조하십시오.의존형 compar 비교 및 자동정리 증명 compar 비교
이름. 최신 버전 개발자 구현 언어 특징들
고차 논리 종속 유형 작은 커널 실증 자동화 반사에 의한 증명 코드 생성
ACL2 8.3 맷 카우프만과 J 스트로터 무어 일반적인 리스프 아니요. 타이프 없음 아니요. 네. 네, 그렇습니다[1]. 이미 실행 가능한 파일
아그다 2.6.2 울프 노렐, 닐스 다니엘슨, 안드레아스 아벨(찰머스와 예테보리) 하스켈 네. 네. 네. 아니요. 부분적 이미 실행 가능한 파일
알바트로스 0.4 헬무트 브란들 OCaml 네. 아니요. 네. 네. 불명 미실장
동작 8.15.2 인리아 OCaml 네. 네. 네. 네. 네. 네.
F* 저장소 Microsoft Research 및 INRIA F* 네. 네. 아니요. 네. 네, 그렇습니다[2]. 네.
홀 라이트 저장소 존 해리슨 OCaml 네. 아니요. 네. 네. 아니요. 아니요.
홀4 Kananaskis-13(또는 repo) 마이클 노리쉬, 콘라드 슬린드 외 표준 ML 네. 아니요. 네. 네. 아니요. 네.
이드리스 2 0.4.0. 에드윈 브래디 이드리스 네. 네. 네. 불명 부분적 네.
이사벨 이자벨2021 (2021년 2월) Larry Paulson(캠브리지), Tobias Nipkow(München), Makarius Wenzel 표준 ML, Scala 네. 아니요. 네. 네. 네. 네.
희박하다 v3.4.2 (공식 릴리즈)[3]v3.39.1 (프리 릴리즈)[4]v4.0.0-m3 (프리 릴리즈)[5] Leonardo de Moura (마이크로소프트 리서치) C++ 네. 네. 네. 네. 네. 불명
LEGO(Lego와 제휴하지 않음) 1.3.1 랜디 폴락(에딘버그) 표준 ML 네. 네. 네. 아니요. 아니요. 아니요.
미자르 8.1.05 비아위스토크 대학교 프리 파스칼 부분적 네. 아니요. 아니요. 아니요. 아니요.
NuPRL 5 코넬 대학교 일반적인 리스프 네. 네. 네. 네. 불명 네.
PVS 6.0 SRI 인터내셔널 일반적인 리스프 네. 네. 아니요. 네. 아니요. 불명
트웰프 1.7.1 프랑크 페닝과 카스텐 쉬르만 표준 ML 네. 네. 불명 아니요. 아니요. 불명
  • ACL2 – Boyer-Moore 전통에서 프로그래밍 언어, 1차 논리 이론 및 정리 프로버(인터랙티브 모드와 자동 모드 모두 포함)
  • Coq – 수학적 어설션의 표현을 허용하고, 이러한 어설션의 증명서를 기계적으로 체크하며, 공식 증명서를 찾는 데 도움이 되며, 공식 명세서의 구성 증명에서 인증된 프로그램을 추출합니다.
  • HOL 정리 프로버– 최종적으로 LCF 정리 프로버에서 파생된 도구 패밀리.이러한 시스템에서 논리 코어는 프로그래밍 언어의 라이브러리입니다.요약은 언어의 새로운 요소를 나타내며 논리적 정확성을 보장하는 "전략"을 통해서만 도입할 수 있습니다.전략 구성은 사용자에게 시스템과의 상호작용이 비교적 적은 상태에서 중요한 증거를 제시할 수 있는 능력을 제공합니다.패밀리의 구성원은 다음과 같습니다.
    • HOL4 – 아직 개발 중인 "프라이머리 후손"Moscow ML과 Poly/ML을 모두 지원합니다. BSD 스타일의 라이선스가 있습니다.
    • HOL Light – 번창하는 "미니멀리스트 포크"입니다.OCaml 기반
    • Proof Power – 독자 사양이 되어 오픈 소스로 돌아갔습니다.표준 ML을 기반으로 합니다.
  • IPS, 대화형 수학 증명 시스템[6]
  • Isabelle은 HOL의 후계자인 인터랙티브 정리 프로버입니다.기본 코드 베이스는 BSD 라이선스이지만 Isabel 디스트리뷰션에서는 여러 애드온툴을 다른 라이선스로 번들합니다.
  • Jape – Java 기반.
  • 희박하다
  • 레고
  • 마티타 – 유도구조의 미적분에 기초한 조명계.
  • MINLOG – 1차 최소 논리에 기반한 증명 도우미.
  • Mizar – 1차 논리와 타르스키-그로텐디크 집합론에 기초한 증명 보조.
  • PhoX – eXtensible인 고차 로직을 기반으로 한 프루프 어시스턴트.
  • PVS(Protype Verification System) – 고차 로직을 기반으로 한 입증 언어 및 시스템.
  • TPS 및 ETPS – 인터랙티브 정리 프로버는 단순한 유형의 람다 미적분을 기반으로 하지만 논리 이론의 독립적 공식과 독립적 구현에 기초합니다.
  • 타입랩
  • 야로

The Orem Prover Museum은 미래 분석을 위해 정리 Prover 시스템의 출처를 보존하기 위한 이니셔티브입니다. 왜냐하면 그것들은 중요한 문화적/과학적인 예술품이기 때문입니다.이것은 위에서 언급한 많은 시스템의 소스를 가지고 있습니다.

사용자 인터페이스

에든버러 대학에서 개발된 Emacs 기반의 Proof General은 교정 보조원들에게 인기 있는 프런트 엔드입니다.Coq에는 Coq가 포함됩니다.OCaml/Gtk에 기반한 IDE.Isabelle은 jEdit 및 Isabel/Scala 인프라스트럭처를 기반으로 문서 지향적인 증명 처리를 위한 Isabelle/jEdit을 포함합니다.최근에는 마카리우스 [7]웬젤에 의해 이자벨을 위한 비주얼 스튜디오 코드 확장도 개발되었습니다.

「 」를 참조해 주세요.

메모들

  1. ^ 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. Vol. 3603. pp. 163–178. doi:10.1007/11541868_11. ISBN 978-3-540-28372-0.
  2. ^ "반사에 의한 증명" 검색: arXiv:1803.06547
  3. ^ "Lean Theorem Prover Releases page". GitHub.
  4. ^ "Lean Community Releases Page". GitHub.
  5. ^ "Lean 4 Releases Page". GitHub.
  6. ^ 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. S2CID 3084322. Retrieved 22 January 2020.
  7. ^ Wenzel, Makarius. "Isabelle". Retrieved 2 November 2019.

레퍼런스

외부 링크

카탈로그