HOL(증거보조)

HOL (proof assistant)
홀
설계자마이클 J C 고든
면허증수정된 (3-클라우드) BSD 라이센스
파일 이름 확장명.sml
웹사이트hol-theorem-prover.org

HOL(Higher Order Logic)은 유사한 (Higher-Order Logic) 로직과 실행 전략을 사용하는 대화형 정리 증명 시스템 계열을 의미한다.이 계열의 시스템은 LCF 접근방식을 따르며, 이러한 유형의 새로운 개체는 고차원의 논리에서 추론 규칙에 해당하는 라이브러리의 기능을 통해서만 생성될 수 있도록 증명된 이론의 추상적 데이터 유형을 정의하는 라이브러리로서 구현된다.이러한 기능이 올바르게 구현되는 한 시스템에서 입증된 모든 이론은 유효해야 한다.이처럼 작은 신뢰의 커널 위에 큰 시스템을 구축할 수 있다.

HOL 계열의 시스템은 ML 또는 그 후계자를 사용한다.ML은 원래 정리 증명 시스템을 위한 메타 언어로서 LCF와 함께 개발되었다. 사실 그 이름은 "메타 언어"를 의미한다.

기초논리학

HOL 시스템은 공리가 거의 없는 단순한 자명적 기초와 잘 이해된 의미론들을 가진 고전적인 고차원의 논리를 사용한다.[1]

HOL 프로버스에 사용되는 논리는 이사벨/HOL과 밀접하게 연관되어 있는데,[2] 이사벨의 논리는 가장 널리 사용되는 논리다.

HOL 구현

비록 HOL은 이사벨의 전신이지만, 다양한 HOL 파생상품은 여전히 활발하고 사용 중이다.다음은 4개의 현재 HOL 시스템(기본적으로 동일한 논리 공유):

  1. HOL4 - Mike Gordon이 주도한 원래의 HOL 구현 노력의 정점이었던 HOL88 시스템에서 기인한 현재 유지 및 개발된 유일한 시스템.HOL88은 Common Lisp 위에 차례로 구현된 자체 ML 구현을 포함했다.HOL88(HOL90, HOL98, HOL4)을 따르는 시스템은 모두 표준 ML에서 구현되었다. 반면 HOL98은 모스크바 ML 또는 Poly/ML로 구축될 수 있다. 모두 매우 단순한 코어 코드 위에 추가적인 자동화를 구현하는 대형 정리 증명 코드 라이브러리가 있다.HOL4는 BSD 면허다.[3]
  2. HOL Light - 실험적으로 "미니멀리스트" 버전의 HOL은 그 이후 또 다른 주류 HOL 변형으로 성장해 왔으며, 그 논리적 기초는 유달리 단순하다.원래 Caml Light에서 구현된 HOL Light는 OCaml을 사용한다.HOL Light는 새로운 BSD 라이선스로 이용할 수 있다.[4]
  3. ProofPower - 공식 사양에 대한 Z 표기법 작업을 위한 특별한 지원을 제공하도록 설계된 도구 모음입니다.6개의 도구 중 5개는 GNU GPL v2 라이센스다.6번째(PDAZ)는 독점 라이선스를 가지고 있다.[5]
  4. HOL Zero - 신뢰도에 초점을 맞춘 미니멀리즘 구현.HOL Zero는 GNU GPL 3+ 라이센스 입니다.[6]

형식 증명 개발

KakeML 프로젝트는 공식적으로 검증된 ML용 컴파일러를 개발했다.[7] 이전에는, HOL은 ARM, x86, PowerPC에서 실행되는 공식적으로 검증된 Lisp 구현을 개발하는데 사용되었다.[8]

또한 HOL은 x86 멀티프로세서의[9] 의미론뿐만 아니라 Power ISA와 ARM 아키텍처의 기계 코드를 공식화하는 데도 사용되었다.[10]

참조

  1. ^ Andrews, Peter B (2002). An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series. Vol. 27 (Second ed.). Dordrecht: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
  2. ^ Tobias Nipkow; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1.
  3. ^ "HOL Interactive Theorem Prover".
  4. ^ "HOL Light".
  5. ^ "Getting ProofPower".
  6. ^ 웨이백 머신에 보관된 2012-03-03 tarball의 라이센스 파일을 참조하십시오.
  7. ^ "CakeML".
  8. ^ Magnus O. Myreen; Michael J. C. Gordon. Verified LISP Implementations on ARM, x86 and PowerPC (PDF). TPHOLs 2009. pp. 359–374.
  9. ^ Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). "x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors" (PDF). Communications of the ACM. 53 (7): 89–97. doi:10.1145/1785414.1785443. S2CID 1999974.
  10. ^ Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009. pp. 13–24.

추가 읽기

외부 링크