証明アシスタント

コンピュータサイエンスと数理論理学において、証明支援装置または対話型定理証明器は、人間と機械の共同作業による正式な証明の開発を支援するソフトウェアツールです。これには、何らかの対話型証明エディタまたはその他のインターフェイスが含まれ、人間はこれを使用して証明の検索をガイドできます。証明の詳細はコンピュータに保存され、いくつかの手順はコンピュータによって提供されます。

この分野における最近の取り組みとしては、これらのツールに人工知能を利用して通常の数学の形式化を自動化することが挙げられる。^[1]

• ACL2  – Boyer-Moore の伝統に基づくプログラミング言語、一階論理理論、定理証明器 (対話型モードと自動モードの両方)。
• Coq  – 数学的な主張の表現を可能にし、これらの主張の証明を機械的にチェックし、形式的な証明を見つけるのを助け、形式仕様の構築的な証明から認定されたプログラムを抽出します。
• HOL 定理証明器– LCF 定理証明器 から最終的に派生したツール ファミリ。これらのシステムでは、論理コアはプログラミング言語のライブラリです。定理は言語の新しい要素を表し、論理的な正しさを保証する「戦略」を通じてのみ導入できます。戦略構成により、ユーザーはシステムとのやり取りを比較的少なくして、重要な証明を作成できます。ファミリのメンバーは次のとおりです。
  • HOL4  – 「主要な後継」であり、現在も活発に開発中です。Moscow MLとPoly/ML の両方をサポートします。BSDスタイルのライセンスがあります。
  • HOL Light  – 活気のある「ミニマリストフォーク」。OCamlベース。
  • ProofPower – 独自仕様になった後、オープンソースに戻りました。Standard MLに基づいています。
• IMPS、対話型数学証明システム。^[8]
• Isabelle は対話型の定理証明器であり、HOL の後継です。メインのコードベースは BSD ライセンスですが、Isabelle ディストリビューションにはさまざまなライセンスのアドオン ツールが多数バンドルされています。
• Jape  – Java ベース。
• 傾く
• レゴ
• Matita  – 帰納的構成の計算に基づいた軽量システム。
• MINLOG  – 一次最小論理に基づく証明支援ツール。
• Mizar –自然演繹スタイル の一階述語論理とTarski-Grothendieck 集合論に基づく証明支援ツール。
• PhoX  – 拡張可能な高階論理に基づく証明アシスタント。
• プロトタイプ検証システム(PVS) – 高階論理に基づく証明言語とシステム。
• TPSと ETPS – 単純型ラムダ計算に基づく対話型定理証明器ですが、論理理論の独立した定式化と独立した実装に基づいています。

証明支援システムの人気のあるフロントエンドは、エディンバラ大学で開発されたEmacsベースの Proof Generalです。

CoqにはOCaml/ GtkをベースにしたCoqIDEが含まれています。Isabelleには、jEditとドキュメント指向の証明処理のためのIsabelle/ ScalaインフラストラクチャをベースにしたIsabelle/jEditが含まれています。最近では、Coq用のVisual Studio Code拡張機能が開発されました。^[9] IsabelleはMakarius Wenzelによって開発されました。 ^{[10] Lean 4用の}Visual Studio Code拡張機能はleanprover開発者によって開発されました。^[11]

Freek Wiedijkは、よく知られている100の定理のリストから定理が形式化されたものの量によって証明支援システムのランキングを作成しています。2023年9月現在、定理の70％以上の証明を形式化しているのは、Isabelle、HOL Light、Coq、Lean、Metamathの5つのシステムのみです。^{[12] [13]}

以下は、証明支援系内で形式化された注目すべき証明のリストです。

• 自動定理証明 – 自動推論と数学的論理のサブフィールド
• コンピュータ支援証明 – 少なくとも部分的にコンピュータによって生成された数学的証明
• 形式検証 – 特定のアルゴリズムの正しさを証明または反証すること
• QED マニフェスト – すべての数学的知識をコンピュータベースでデータベース化する提案
• 理論による充足可能性 – コンピュータサイエンスで研究される論理的問題
• Prover9 –一階述語論理と等式論理の自動定理証明器です

• Barendregt, Henk ; Geuvers, Herman (2001)。「18. 依存型システムを使用した証明支援」(PDF)。Robinson, Alan JA、Voronkov, Andrei (編)。自動推論ハンドブック。第 2 巻。Elsevier。pp. 1149– 。ISBN 978-0-444-50812-62007年7月27日時点のオリジナル（PDF）よりアーカイブ。
• Pfenning, Fr​​ank . 「17. 論理フレームワーク」(PDF) .ハンドブック第 2 巻 2001 年. pp.  1065– 1148.
• Pfenning, Fr​​ank (1996)。「論理フレームワークの実践」。Kirchner, H. (編)。代数とプログラミングにおけるツリー - CAAP '96 。コンピュータサイエンスの講義ノート。第 1059 巻。Springer。pp.  119– 134。doi : 10.1007 /3-540-61064-2_33。ISBN 3-540-61064-2。
• Constable, Robert L. (1998)。「X. コンピュータサイエンス、哲学、論理における型」Buss, SR (編)。証明理論ハンドブック。論理学研究。第 137 巻。エルゼビア 。683 ～ 786ページ。ISBN 978-0-08-053318-6。
• ヴィーダイク、フリーク (2005)。 「世界の17の証明者」(PDF)。ラドボウド大学ナイメーヘン校。

• 定理証明博物館
• 依存型を使用した認定プログラミングの「概要」。
• Coq 証明アシスタントの紹介 (対話型定理証明の一般的な紹介付き)
• Agda ユーザーのためのインタラクティブな定理証明
• 定理証明ツールのリスト

カタログ

• カテゴリー別デジタル数学: 戦術証明者
• 自動控除システムとグループ
• 定理証明と自動推論システム
• 既存の機械化推論システムのデータベース
• NuPRL: その他のシステム
• 「特定の論理フレームワークと実装」。2022年4月10日時点のオリジナルよりアーカイブ。2024年2月15日閲覧。（フランク・フェニング著）。
• DMOZ : 科学: 数学: 論理と基礎: 計算論理: 論理フレームワーク