HOL（証明支援系）
ホール
デザイン：マイケル・J・C・ゴードン
ライセンス修正（3条項）BSDライセンス
ファイル名拡張子.sml
Webサイトhol-theorem-prover.org​

HOL（高階論理）は、類似した（高階）論理と実装戦略を用いた対話型定理証明システムのファミリーを指します。このファミリーのシステムは、 LCF （計算可能関数のための論理）アプローチに従っており、証明された定理の抽象データ型を定義するライブラリとして実装されています。このタイプの新しいオブジェクトは、高階論理の推論規則に対応するライブラリ内の関数を使用してのみ作成できます。これらの関数が正しく実装されている限り、システムで証明されたすべての定理は有効である必要があります。そのため、小規模で信頼できるカーネル上に大規模なシステムを構築することができます。

HOLファミリーのシステムはMLまたはその後継言語を使用します。MLは元々、定理証明システムのためのメタ言語としてLCFとともに開発されました。実際、その名前は「Meta-Language（メタ言語）」の略です。

根底にある論理

HOLシステムは古典的な高階論理の変種を使用しており、これは公理が少なく意味論がよく理解された単純な公理的基礎を持っています。[ 1 ]

HOL証明器で使用されるロジックは、Isabelleの最も広く使用されているロジックであるIsabelle/HOL [ 2 ]と密接に関連しています。

HOL実装

数多くの HOL システム (本質的に同じロジックを共有) がアクティブのまま使用中です。

  1. HOL4 — 現在保守・開発が行われている唯一のシステムで、マイク・ゴードンが率いたオリジナルのHOL実装の集大成であるHOL88システムから派生したものです。HOL88には独自のML実装が含まれており、これはCommon Lisp上に実装されていました。HOL88に続くシステム（HOL90、hol98、HOL4）はすべてStandard MLで実装されていました。hol98はMoscow MLと連携していますが、HOL4はMoscow MLまたはPoly/MLのいずれかで構築できます。すべてに、非常にシンプルなコアコード上に追加の自動化を実装する大規模な定理証明コードライブラリが付属しています。HOL4はBSDライセンスです。[ 3 ]
  2. HOL Light — HOLの実験的な「ミニマリスト」バージョンで、後に主流のHOLの亜種へと成長しました。その論理的基盤は驚くほどシンプルです。HOL Lightは元々Caml Lightで実装されていましたが、現在はOCamlを使用しています。HOL Lightは新しいBSDライセンスの下で利用可能です。[ 4 ]
  3. ProofPower — HOLを基盤としたZ記法を用いた形式仕様記述のための特別なサポートを提供する6つのツール群です。Adaのサブセットで記述されたプログラムの仕様記述と検証をサポートするツールPPDazは、以前はプロプライエタリライセンスのみで提供されていました。現在、すべてのツールはGNU GPL v2ライセンスで利用可能です。
  4. HOL Zero — 信頼性を重視したミニマリスト実装。HOL ZeroはGNU GPL 3+ライセンスです。[ 5 ]
  5. Candle — CakeML上にエンドツーエンドで検証されたHOL Light実装。[ 6 ]

形式的証明の発展

CakeMLプロジェクトは、 ML用の正式に証明されたコンパイラを開発しました。[ 7 ]以前は、HOLを使用して、ARM、x86、PowerPCで動作する正式に証明されたLisp実装を開発しました。[ 8 ]

HOLはx86マルチプロセッサのセマンティクス[ 9 ]やPower ISAおよびARMアーキテクチャのマシンコードを形式化するためにも使用されました[ 10 ] 。

参考文献

  1. ^アンドリュース、ピーター・B (2002). 『数理論理学と型理論入門：証明を通して真理へ』応用論理シリーズ. 第27巻（第2版）. ドルドレヒト：クルーワー・アカデミック・パブリッシャーズ. 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インタラクティブ定理証明器」。
  4. ^ 「HOLライト」。
  5. ^ tarball内の LICENSE ファイルを参照してください。2012 年 3 月 3 日にWayback Machineにアーカイブされています。
  6. ^ Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andronick, June; de Moura, Leonardo (編). "Candle: A Verified Implementation of HOL Light" .第13回国際インタラクティブ定理証明会議 (ITP 2022) . Leibniz International Proceedings in Informatics (LIPIcs). 237.ダグストゥール, ドイツ: Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 3:1–3:17. doi : 10.4230/LIPIcs.ITP.2022.3 . ISBN 978-3-95977-252-5. S2CID  251323103 .
  7. ^ 「CakeML」。
  8. ^ Magnus O. Myreen; Michael JC Gordon. ARM、x86、PowerPCにおける検証済みLISP実装(PDF) . TPHOLs 2009. pp.  359– 374.
  9. ^ Peter Sewell、Susmit Sarkar、Scott Owens、Francesco Zappa Nardelli、Magnus O. Myreen (2010). 「x86-TSO：x86マルチプロセッサ向けの厳密かつ使いやすいプログラマモデル」（PDF） . Communications of the ACM . 53 (7): 89– 97. doi : 10.1145/1785414.1785443 . S2CID 1999974 . 
  10. ^ Jade Alglave、Anthony CJ Fox、Samin Ishtiaq、Magnus O. Myreen、Susmit Sarkar、Peter Sewell、Francesco Zappa Nardelli. PowerとARMマルチプロセッサマシンコードのセマンティクス（PDF） . DAMP 2009. pp.  13– 24.

さらに読む

「 https://en.wikipedia.org/w/index.php?title=HOL_(proof_assistant)&oldid=1305058799」から取得