HOL（校正アシスタント）

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

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

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

HOL証明器で使用される論理は、Isabelle/HOL ^{[ 2 ]}と密接に関連しており、 Isabelleで最も広く使用されている論理です。

基本的に同じロジックを共有する複数の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 バリアントへと成長しました。その論理的基盤は、非常にシンプルです。元々はCaml Lightで実装されていた HOL Light は、現在OCaml を使用しています。HOL Light は、新しい BSD ライセンスの下で利用可能です。^{[ 4 ]}
3. ProofPowerは、形式仕様記述のためのZ記法を扱う際に、HOLに基づいた特別なサポートを提供するように設計された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 ] 。}

• ゴードン、マイケル JC (1996)。「LCF から HOL へ：短い歴史」。2007年 10 月 11 日に取得。

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