이사벨(프루프 어시스턴트)

Isabelle (proof assistant)
이사벨
Isabelle jedit.png
MacOS에서 실행되는 Isabelle/jEdit
원저작자로렌스 폴슨
개발자케임브리지 대학과 뮌헨 공과대학 등
초기 릴리즈1986년[1]
안정된 릴리스
이자벨2021 / 2021년 2월, 1년 전(2021-02)
기입처표준 ML 및 스칼라
운영 체제Linux, Windows, MacOS
유형수학
면허증.BSD 라이선스
웹 사이트isabelle.in.tum.de

이자벨[a] 자동 정리 계산기는 표준 ML 및 스칼라로 작성된 고차 논리(HOL) 정리 계산기입니다.LCF 스타일의 정리 프로버로서 명시적 증명 오브젝트를 필요로 하지 않고(그러나 지원하지 않고) 증명의 신뢰성을 높이기 위해 작은 논리 코어(커널)를 기반으로 합니다.

Isabelle은 논리적으로 안전한 확장을 가능하게 하는 유연한 시스템 프레임워크 내에서 사용할 수 있습니다.이러한 확장 기능은 코드 생성, 문서화 및 다양한 공식 방법에 대한 특정 지원을 위한 구현뿐만 아니라 이론으로 구성됩니다.정식 메서드의 IDE로 볼 수 있습니다.최근 몇 년 동안, 상당한 수의 이론과 시스템 확장이 이자벨 공식 증거 아카이브(Isabelle AFP)[2]에 수집되었다.

이사벨은 로렌스 폴슨에 의해 제라르 휴의 [3]딸의 이름을 따서 지어졌다.

Isabelle 정리 프로버는 개정된 BSD 라이선스로 출시된 자유 소프트웨어입니다.

특징들

이자벨은 일반적이다: 이것은 1차 논리(FOL), 고차 논리(HOL), 저멜로-프랭클 집합 이론(ZFC)과 같은 객체 논리학을 인코딩하는데 사용된다.이자벨/ZF에서 상당한 집합론 개발이 완료되었지만, 가장 널리 사용되는 개체 논리는 이자벨/HOL이다.Isabelle의 주요 증명 방법은 고차 통일에 기초한 고차 버전의 해상도입니다.

대화적이긴 하지만 Isabelle은 용어 재작성 엔진, 테이블로프로버, 다양한 의사결정 절차, Slegehammer proof-Automation 인터페이스를 통해 외부 만족도 모듈로 이론(CVC4 포함) 및 분해능 기반 자동 정리프로버(ATPs)와 같은 효율적인 자동 추론 도구를 갖추고 있습니다.NG E 및 SPASS(메티스[b] 증명 방법은 이러한 ATP에 [4]의해 생성된 분해능 증명을 재구성합니다.)또, 다음의 2개의 모델 파인더(카운터 샘플 생성기)도 갖추고 있습니다.니트픽과[5] 논차쿠.[6]

이사벨은 큰 증거를 구성하는 모듈인 로케일을 특징으로 합니다.로케일은 지정된 범위[5] 내에서 유형, 상수 및 가정을 수정하여 모든 보조 프로그램에 대해 반복할 필요가 없도록 합니다.

이자르(이해할 수 있는 반자동 추리)는 이자벨의 공식 증명 언어이다.그것은 미자르 [5]시스템에서 영감을 얻었다.

증거의 예

이사벨은 증명이 절차적 문체와 선언적 문체의 두 가지 다른 문체로 쓰여질 수 있도록 허락한다.절차 증명은 적용할 일련의 전술(테마 증명 함수/절차)을 명시한다.인간 수학자가 결과를 증명하기 위해 적용할 수 있는 절차를 반영하지만, 일반적으로 이러한 단계의 결과를 설명하지 않기 때문에 읽기 어렵다.반면에 선언적 증명(이사벨의 증명 언어, 이자르에 의해 지원됨)은 수행되어야 할 실제 수학 연산을 지정하며, 따라서 인간이 더 쉽게 읽고 확인할 수 있습니다.

이사벨의 [citation needed]최근 버전에서는 절차 방식이 더 이상 사용되지 않는다.

예를 들어, 2의 제곱근이 유리하지 않다는 이자르에서의 모순에 의한 선언적 증명은 다음과 같이 쓸 수 있다. 

정리 sqrt2_not_div: "rt2 ∉ ℚ ℚ ℚ" 증명 ?x = "rt2"는 "?x ∈ ℚ"로 가정하고 m n :: nat을 구합니다.여기서 sqrt_rt: "rt?"x = "m / n" 및 lowest_rt: "coprime mn" by: "rt: "n" by Rat_abs_n"는 "rets_n"이다.ence "2 dvd m^2" by simp. 따라서 "2 dvd m"은 "2 dvd n" 증명이 된다. δ2 dvd m obtain obtain = 2 * k 。 eq는 "2 * n^2 = 2^2 * k^2" by simp"를 가지므로 dvd "2 dvd n2"는 dvd m" 증명이 된다.홀수_1 사용

적용들

Isabelle은 소프트웨어 및 하드웨어 시스템의 사양, 개발 및 검증을 위한 공식적인 방법을 지원하기 위해 사용되어 왔습니다.

이자벨은 선택 공리의 일관성, 소수 정리, 보안 프로토콜의 정확성, 프로그래밍 언어 의미론의 특성에 대한 Gödel의 정리와 같은 수학과 컴퓨터 과학으로부터 수많은 이론들을 공식화하는데 사용되어 왔다.언급한 바와 같이 공식 증거의 대부분은 총 [7]200만 줄 이상의 증거를 가진 최소 500개의 문서를 포함하는 형식 증거 보관소에 보관되어 있다.

  • 2009년 NICTA의 L4.검증된 프로젝트는 범용 운영체제 [8]커널인 seL4(시큐어 임베디드 L4) 마이크로커널의 기능적 정확성에 대한 최초의 공식 증명서를 작성했습니다.증명은 Isabelle/HOL에서 작성 및 확인되며 C의 7,500 행을 검증하기 위한 200,000 행 이상의 증명 스크립트로 구성됩니다.검증은 코드, 설계 및 구현을 포함하며, 주요 정리는 C 코드가 커널의 정식 사양을 올바르게 구현한다는 것입니다.seL4 커널의 C 코드 초기 버전에서 144개의 버그가 발견되었으며 설계 및 사양 각각에서 약 150개의 문제가 발견되었습니다.

래리 폴슨은 이사벨을 [10]이용한 연구 프로젝트 목록을 가지고 있다.

대체 수단

상세정보 : Proof Assistant system시스템 비교

여러 언어와 시스템에서 동일한 기능을 제공합니다.

메모들

  1. ^ /sncz-bb/
  2. ^ /440mi/

레퍼런스

  1. ^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4. S2CID 27085090.
  2. ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 1 May 2021.
  3. ^ Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Retrieved 2016-04-28.
  4. ^ Jasmin Christian Blanchette, Lukas Bulwan, Tobias Nipkow, "Automatic Proof and Infloof in Isabelle/HOL", Cesare Tinelli, Viorica Sofronie-Stokkermans, Froco 통합 시스템 프런티어에 관한 국제 심포지엄 2011.
  5. ^ a b c Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach, "학습, 망각, 재시작 및 증분성을 포함한 검증된 SAT 해결사 프레임워크", 자동 추론 저널 61:333–365(2018).
  6. ^ Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli, "SMT의 재귀적 기능에 대한 모델 발견", "Nicola Olivetti, Ashish Tiwari(eds), 제8회 자동 추리 국제 공동 회의, Springer, 2016.
  7. ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 22 October 2019.
  8. ^ Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, Montana, US. pp. 207–200.
  9. ^ Strniša, Rok; Parkinson, Matthew (2011-02-07). "Lightweight Java". Archive of Formal Proofs (Feb 2011 ed.). ISSN 2150-914X. Retrieved 2019-11-25.
  10. ^ "Projects - Isabelle Community Wiki".

추가 정보

외부 링크