イザベル（校正アシスタント）

イザベル
	Isabelle – macOSで動作する jEdit
原作者	ローレンス・ポールソン
開発者	ケンブリッジ大学、; ミュンヘン工科大学、その他
初回リリース	1986年; 38年前
安定リリース	Isabelle2024 / 2024年5月; 7か月前
書かれた	標準 ML、Scala
オペレーティング·システム	Linux、Windows、macOS
タイプ	数学
ライセンス	BSDA の
Webサイト	イザベル

Isabelle ^[a]自動定理証明器は、Standard MLとScalaで記述された高階論理 (HOL) 定理証明器です。計算可能関数の論理(LCF) スタイルの定理証明器として、明示的な証明オブジェクトを必要とせずに (サポートすることなく) 証明の信頼性を高めるために、小さな論理コア (カーネル) に基づいています。

Isabelleは、コード生成、文書化、およびさまざまな形式手法の特定のサポートのための理論と実装の両方を含む、論理的に安全な拡張を可能にする柔軟なシステムフレームワーク内で利用できます。これは、形式手法の統合開発環境（IDE）と見なすことができます。近年、かなりの数の理論とシステム拡張がIsabelle Archive of Formal Proofs（Isabelle AFP）^[2]に収集されています。

イザベルはジェラール・ユエの娘にちなんでローレンス・ポールソンによって名付けられました。 ^[3]

Isabelle 定理証明器は、改訂BSD ライセンスに基づいてリリースされたフリーソフトウェアです。

特徴

Isabelle は汎用的です。Isabelle はメタロジック(弱い型理論)を提供し、これを使用して一階述語論理(FOL)、高階論理(HOL)、ツェルメロ-フランケル集合論(ZFC) などのオブジェクトロジックをエンコードします。最も広く使用されているオブジェクトロジックは Isabelle/HOL ですが、重要な集合論の開発は Isabelle/ZF で完了しました。Isabelle の主な証明方法は、高階統一に基づく、解像度の高階バージョンです。

Isabelle は対話型でありながら、項書き換えエンジンやタブロー証明器などの効率的な自動推論ツール、さまざまな決定手順、およびSledgehammer証明自動化インターフェースを介した外部充足可能性法理論(SMT) ソルバー ( CVC4を含む) とE、SPASS、Vampireなどの解決ベースの自動定理証明器(ATP) を備えています( Metis ^[b]証明方法は、これらの ATP によって生成された解決証明を再構築します)。^[4]また、Nitpick ^[5]とNunchakuという 2 つのモデルファインダー (反例生成器)も備えています。^[6]

Isabelleは、大規模な証明を構造化するモジュールであるロケールを備えています。ロケールは、指定されたスコープ^{[5]内で型、定数、仮定を固定するため、すべての}補題で繰り返す必要がありません。

Isar（「理解可能な半自動推論」）はIsabelleの形式証明言語である。これはMizarシステムに触発されている。^[5]

証明例

Isabelle では、手続き型と宣言型の2 つの異なるスタイルで証明を記述できます。手続き型証明では、適用する一連の戦術 (定理証明関数/手順) を指定します。人間の数学者が結果を証明するために適用する手順を反映していますが、これらの手順の結果が記述されていないため、通常は読みにくいです。一方、宣言型証明 (Isabelle の証明言語 Isar でサポート) では、実行される実際の数学演算を指定するため、人間が読みやすく、確認しやすくなります。

手続き型スタイルは、Isabelle の最近のバージョンでは非推奨になりました。^{[引用が必要]}

たとえば、2 の平方根が有理数ではないという Isar の背理法による宣言的証明は次のように記述できます。

定理sqrt2_not_rational:
   "sqrt 2 ∉ ℚ"
証明?x = "sqrt 2"と仮定"?x ∈ ℚ"とすると、 mn :: natが得られます。ここで、 
    sqrt_rat: "¦?x¦ = m / n"であり、 lowest_terms: "互いに素な m n" (rule Rats_abs_nat_div_natE)
  であるため、"m^2 = ?x^2 * n^2" (auto simp add: power2_eq_square)
  であるため、 eq: "m^2 = 2 * n^2" of_nat_eq_iff power2_eq_squareを使用fastforce
  であるため、"2 dvd m^2" ( simp
  により) であるため、"2 dvd m" ( simp
  により) であるため、"2 dvd n"となります証明-
     ‹2 dvd m›からkが得られます。
    ここで、"m = 2 * k"です。eqは次のようになります。 simp
    により「2 * n^2 = 2^2 * k^2」となり、したがってsimp
    により「2 dvd n^2」となり、したがってsimpにより「2 dvd n」となり、‹2 dvd m›によりsimp
   qed され、 (rule gcd_greatest)
  によりlowest_termsにより「2 dvd gcd m n」となり、 simp
  により「2 dvd 1」となり、したがってblast
 qedによりodd_one を使用してFalse となる

アプリケーション

Isabelle は、ソフトウェアおよびハードウェアシステムの仕様、開発、検証のための形式手法を支援するために使用されてきました。

Isabelleは、ゲーデルの完全性定理、選択公理の一貫性に関するゲーデルの定理、素数定理、セキュリティプロトコルの正しさ、プログラミング言語セマンティクスの特性など、数学やコンピュータサイエンスの数多くの定理を形式化するために使用されてきました。前述のように、形式的な証明の多くは、Archive of Formal Proofsで管理されており、そこには（2019年現在）少なくとも500の記事と合計200万行を超える証明が含まれています。^[7]

2009年、 NICTAのL4.verifiedプロジェクトは、汎用オペレーティングシステムカーネルの機能的正しさの最初の正式な証明を作成しました：^[8] seL4（セキュア組み込みL4）マイクロカーネル。証明はIsabelle/HOLで構築およびチェックされ、7,500行のCを検証するための200,000行を超える証明スクリプトで構成されています。検証はコード、設計、実装をカバーし、主な定理はCコードがカーネルの形式仕様を正しく実装していると述べています。証明では、seL4カーネルのCコードの初期バージョンに144のバグが見つかり、設計と仕様のそれぞれに約150の問題がありました。

プログラミング言語Lightweight Javaの定義はIsabelleで型通りであることが証明されました。 ^[9]

ラリー・ポールソンは、Isabelle を使用する研究プロジェクトのリストを作成しています。^[10]^{[リンク切れ‍ ]}

代替案

いくつかの言語とシステムが同様の機能を提供しています。

注記

^ / ˌ ɪ z ə ˈ b ɛ l /
^ / ˈ m iː t ɪ s /

参考文献

^ Paulson, LC (1986). 「高階解決としての自然演繹」. The Journal of Logic Programming . 3 (3): 237–258. arXiv : cs/9301104 . doi :10.1016/0743-1066(86)90015-4. S2CID 27085090.
^ エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2021 年5 月 1 日に取得。
^ Gordon, Mike (1994-11-16). 「1.2 履歴」Isabelle と HOL。 Cambridge AR Research (The Automated Reasoning Group)。 2017-03-05 時点のオリジナルよりアーカイブ。2016-04-28に取得。
^ Jasmin Christian Blanchette、Lukas Bulwahn、Tobias Nipkow、「Isabelle/HOL における自動証明と反証」、Cesare Tinelli、Viorica Sofronie-Stokkermans (編)、International Symposium on Frontiers of Combining Systems – FroCoS 2011、Springer、2011 年。
^ abc Jasmin Christian Blanchette、Mathias Fleury、Peter Lammich、Christoph Weidenbach、「学習、忘却、再開、増分性を備えた検証済みSATソルバーフレームワーク」、Journal of Automated Reasoning 61 :333–365 (2018)。
^ Andrew Reynolds、Jasmin Christian Blanchette、Simon Cruanes、Cesare Tinelli、「SMT での再帰関数のモデル検索」、Nicola Olivetti、Ashish Tiwari (編)、第 8 回国際自動推論合同会議、Springer、2016 年。
^ エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2019 年10 月 22 日に取得。
^ Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (2009 年 10 月)。「seL4: OS カーネルの形式検証」(PDF)。第 22 回 ACM オペレーティングシステム原則シンポジウム。米国モンタナ州ビッグスカイ。pp. 207–200。
^ Strniša, Rok; Parkinson, Matthew (2011年2月7日). 「Lightweight Java」. Archive of Formal Proofs (2011年2月版). ISSN 2150-914X . 2019年11月25日閲覧。
^ 「プロジェクト - Isabelle コミュニティ Wiki」。

さらに読む

Lawrence C. Paulson、「汎用定理証明器の基礎」、Journal of Automated Reasoning、第 5 巻、第 3 号 (1989 年 9 月)、363 ～ 397 ページ、ISSN 0168-7433。
Lawrence C. Paulson およびTobias Nipkow、「Isabelle チュートリアルおよびユーザーズマニュアル」、1990 年。
MA Ozols、KA Eastaughffe、A. Cant、「DOVE: 設計指向の検証および評価のためのツール」、AMAST 97 の議事録、M. Johnson 編、シドニー、オーストラリア。Lecture Notes in Computer Science (LNCS) Vol. 1349、Springer Verlag、1997 年。
Tobias Nipkow、Lawrence C. Paulson、Markus Wenzel、「Isabelle/HOL – 高階論理の証明アシスタント」、2020 年。

外部リンク

公式サイト
Stack Overflow の Isabelle
形式的証明のアーカイブ
IsarMathLib

[2] / ˌ ɪ z ə ˈ b ɛ l /

[5] / ˈ m iː t ɪ s /

[1] Paulson, LC (1986). 「高階解決としての自然演繹」. The Journal of Logic Programming . 3 (3): 237–258. arXiv : cs/9301104 . doi :10.1016/0743-1066(86)90015-4. S2CID 27085090.

[3] エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2021 年5 月 1 日に取得。

[4] Gordon, Mike (1994-11-16). 「1.2 履歴」Isabelle と HOL。 Cambridge AR Research (The Automated Reasoning Group)。 2017-03-05 時点のオリジナルよりアーカイブ。2016-04-28に取得。

[6] Jasmin Christian Blanchette、Lukas Bulwahn、Tobias Nipkow、「Isabelle/HOL における自動証明と反証」、Cesare Tinelli、Viorica Sofronie-Stokkermans (編)、International Symposium on Frontiers of Combining Systems – FroCoS 2011、Springer、2011 年。

[:0-7] Jasmin Christian Blanchette、Mathias Fleury、Peter Lammich、Christoph Weidenbach、「学習、忘却、再開、増分性を備えた検証済みSATソルバーフレームワーク」、Journal of Automated Reasoning 61 :333–365 (2018)。

[8] Andrew Reynolds、Jasmin Christian Blanchette、Simon Cruanes、Cesare Tinelli、「SMT での再帰関数のモデル検索」、Nicola Olivetti、Ashish Tiwari (編)、第 8 回国際自動推論合同会議、Springer、2016 年。

[9] エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2019 年10 月 22 日に取得。

[Klein_EHACDEEKNSTW_09-10] Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (2009 年 10 月)。「seL4: OS カーネルの形式検証」(PDF)。第 22 回 ACM オペレーティングシステム原則シンポジウム。米国モンタナ州ビッグスカイ。pp. 207–200。

[11] Strniša, Rok; Parkinson, Matthew (2011年2月7日). 「Lightweight Java」. Archive of Formal Proofs (2011年2月版). ISSN 2150-914X . 2019年11月25日閲覧。

[12] 「プロジェクト - Isabelle コミュニティ Wiki」。

特徴

証明例

アプリケーション

代替案

注記

参考文献

さらに読む

外部リンク

関連するトピック

macOSで動作する jEdit

原作者

ローレンス・ポールソン

ケンブリッジ大学、