Isabelle / HOLベリファイアのコアアルゴリズムは何ですか？
スキームメタサーキュラーエバリュエーターのレベルで何かを探しています。
私は検証者にのみ興味があり、自動定理証明の戦略には興味がありません。
簡単な証明検証ツールを最初から実装したい（本番環境ではなく、純粋に教育上の理由で）。
Isabelle/HOLのコアベリファイアアルゴリズムを理解したい。自動定理証明に使用される戦略/コードは気にしません。
コアのVerifierアルゴリズムは非常に単純（かつエレガント）であると思われます。しかし、私はそれを見つけることができません。
ありがとう！
Isabelleは、証明チェッカーの「LCFファミリー」のメンバーです。つまり、抽象データ型の値を生成するためにすべての推論が実行される特別なモジュール（推論カーネル）がありますthm。これは、オペレーティングシステムのカーネル処理システムコールに少し似ています。この方法で作成できるものはすべて、カーネル実装の正確さに比べて「構造上正しい」ものです。証明者のプログラミング言語環境（Standard ML）は、非常に強力な静的型正し性を備えているため、推論カーネルの構築による正しさは、残りの証明アシスタントの実装に引き継がれます。これは非常に大きなものになる可能性があります。
したがって、原則として、比較的小さな「信頼できるカーネル」部分と非常に大きな「アプリケーションユーザースペース」があります。特に、Isabelle / HOLのほとんどは、実際にはIsabelleユーザーランドのライブラリ理論とアドオンツール（主にSML）の大きなコレクションです。
Isabelleでは、カーネルインフラストラクチャは非常に複雑ですが、それでもシステムの他の部分と比較すると非常に小さいです。カーネルは、実際には「マイクロカーネル」（モジュール）と「ナノカーネル」（モジュール）に階層化されていますThm。 ミルナーのLCFアプローチの意味で値を生成し、生成する結果の証明書と、ローカル推論の証明コンテキスト（特にIsar証明言語）を処理します。ContextThmthmContexttheory
LCFスタイルの証明者についてもっと知りたい場合は、おそらくLCFファミリーの中で最小の現実的なシステムであるHOL-Lightも見てみることをお勧めします。これは、人々が大きなアプリケーションを使用しているという意味で現実的です。HOL-Lightには、その実装を簡単に理解できるという大きな利点がありますが、このミニマリズムにはいくつかの欠点もあります。SMLではなくOCamlであるML環境でユーザーが無意味なことをするのを完全に保護するわけではありません。さまざまな技術的な理由から、OCamlはデフォルトではStandardMLほど「安全」ではありません。
Isabelle のソースを untar すると、たとえば
http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
あなたはコア定義を見つけるでしょう
ソース/ピュア/thm.ML
そして、あなたが取り組みたいプロジェクトがすでにあります：
http://www.proof-technologies.com/holzero/
後で追加: 別の、より深刻なプロジェクトは