HOL（証明補助）

ホール
デザイン：	マイケル・J・C・ゴードン
ライセンス	修正（3条項）BSDライセンス
ファイル名拡張子	.sml
Webサイト	定理証明者

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

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

根底にある論理

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

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

HOL実装

いくつかの HOL システム (基本的に同じロジックを共有) が引き続きアクティブで使用されています。

HOL4 — 現在保守・開発されている唯一のシステムで、マイク・ゴードンが率いたオリジナルの HOL 実装の集大成である HOL88 システムから派生したものです。HOL88 には独自のML実装が含まれており、これはCommon Lisp上に実装されていました。HOL88 に続くシステム (HOL90、hol98、HOL4) はすべてStandard MLで実装されました。hol98 はMoscow MLと連動していますが、HOL4 は Moscow ML またはPoly/MLのいずれかで構築できます。すべてに、非常にシンプルなコアコード上に追加の自動化を実装する、定理証明コードの大規模なライブラリが付属しています。HOL4 は BSD ライセンスです。^[3]
HOL Light — HOL の実験的な「ミニマリスト」バージョンで、その後、別の主流の HOL バリアントに成長しました。その論理的基礎は、非常に単純なままです。HOL Light は、もともとCaml Lightで実装されていましたが、現在はOCaml を使用しています。HOL Light は、新しい BSD ライセンスの下で利用できます。^[4]
ProofPower — 形式仕様のZ表記法を扱うための特別なサポートを提供するように設計されたツールのコレクション。6つのツールのうち5つはGNU GPL v2ライセンスです。6番目のツール（PPDaz）はプロプライエタリライセンスです。^[5]
HOL Zero — 信頼性を重視したミニマリスト実装。HOL ZeroはGNU GPL 3+ライセンスです。^[6]
Candle — CakeMLをベースにしたエンドツーエンドで検証されたHOL Light実装。^[7]

形式的証明の発展

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

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

参考文献

^ アンドリュース、ピーター B (2002)。数理論理学と型理論入門：証明を通して真理へ。応用論理シリーズ。第 27 巻（第 2 版）。ドルドレヒト：クルーワーアカデミックパブリッシャーズ。ISBN 978-1-4020-0763-7。
^ Tobias Nipkow、Markus Wenzel、Lawrence C. Paulson (2002)。Isabelle /HOL :高階論理の証明支援ツール。ベルリン、ハイデルベルク: Springer-Verlag。ISBN 978-3-540-45949-1。
^ 「HOL インタラクティブ定理証明器」。
^ 「HOLライト」.
^ 「ProofPowerの入手」。
^ tarball 内の LICENSE ファイルを参照してください。2012-03-03 にWayback Machineにアーカイブされています。
^ Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andronick, June; de Moura, Leonardo (eds.). 「Candle: HOL Light の検証済み実装」.第 13 回国際インタラクティブ定理証明会議 (ITP 2022) . ライプニッツ国際情報学会議 (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。
^ 「CakeML」.
^ Magnus O. Myreen、Michael JC Gordon。ARM、x86、PowerPC での検証済み LISP 実装(PDF)。TPHOLs 2009。pp. 359–374。
^ 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 。
^ 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。

さらに読む

Gordon, Michael JC (1996)。「LCF から HOL まで: 短い歴史」。2007年 10 月 11 日閲覧。

外部リンク

公式サイト
HOLの基本ロジックを規定する文書
HOL4説明マニュアル、システムロジック仕様を含む
仮想ライブラリ形式手法情報

[1] アンドリュース、ピーター B (2002)。数理論理学と型理論入門：証明を通して真理へ。応用論理シリーズ。第 27 巻（第 2 版）。ドルドレヒト：クルーワーアカデミックパブリッシャーズ。ISBN 978-1-4020-0763-7。

[2] Tobias Nipkow、Markus Wenzel、Lawrence C. Paulson (2002)。Isabelle /HOL :高階論理の証明支援ツール。ベルリン、ハイデルベルク: Springer-Verlag。ISBN 978-3-540-45949-1。

[3] 「HOL インタラクティブ定理証明器」。

[4] 「HOLライト」.

[5] 「ProofPowerの入手」。

[6] tarball 内の LICENSE ファイルを参照してください。2012-03-03 にWayback Machineにアーカイブされています。

[7] Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andronick, June; de Moura, Leonardo (eds.). 「Candle: HOL Light の検証済み実装」.第 13 回国際インタラクティブ定理証明会議 (ITP 2022) . ライプニッツ国際情報学会議 (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。

[8] 「CakeML」.

[9] Magnus O. Myreen、Michael JC Gordon。ARM、x86、PowerPC での検証済み LISP 実装(PDF)。TPHOLs 2009。pp. 359–374。

[10] 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 。

[11] 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。