イザベル（校正アシスタント）
イザベル
原作者ローレンス・ポールソン
開発者ケンブリッジ大学、ミュンヘン工科大学、その他
初回リリース1986年[ 1 ] （1986年）
安定版リリース
Isabelle2025 / 2025年3月 （2025年3月）
書かれた標準ML、Scala
オペレーティング·システムLinux、Windows、macOS
タイプ数学
ライセンスBSD
Webサイトイザベル.in .tum .de

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 ]また、2 つのモデル検索器 (反例生成器)、Nitpick [ 5 ]とNunchaku [ 6 ]も備えています。

Isabelle は、大規模な証明を構造化するモジュールであるロケールを備えています。ロケールは、型、定数、および仮定を特定のスコープ[ 5 ]内で固定するため、すべての補題でそれらを繰り返す必要がなくなります。

Isar（「理解可能な半自動推論」）は、Isabelleの形式証明言語です。Mizarシステムに着想を得ています。[ 5 ]

証明例

Isabelleでは、手続き型と宣言型の2つの異なるスタイルで証明を記述できます。手続き型証明では、適用すべき一連の戦術（定理証明関数／手順）を指定します。これは人間の数学者が結果を証明する際に適用する手順を反映していますが、これらの手順の結果が記述されていないため、一般的に読みにくいです。このスタイルはIsabelleのドキュメントで「有害であると見なされている」とされています。[ 7 ]

一方、宣言的証明 (Isabelle の証明言語 Isar でサポート) は、実行される実際の数学演算を指定するため、人間が読みやすく、確認しやすくなります。

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

定理sqrt2_not_rational: "sqrt 2 ∉ ℚ"証明? x = "sqrt 2"と仮定"?x ∈ ℚ"とすると、 mn :: natが得られます。ここで、 sqrt_rat: "¦?x¦ = m / n"かつlowest_terms: "coprime 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›でqed され、 (rule gcd_greatest) により"2 dvd gcd m n"となり、 lowest_termsによりsimp により"2 dvd 1"となり、したがってodd_oneを使用するとblast によりqed され、 False となる

アプリケーション

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

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

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

代替案

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

注記

参考文献

  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 .
  2. ^エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2021 年5 月 1 日に取得。
  3. ^ Gordon, Mike (1994-11-16). 「1.2 歴史」 . Isabelle and HOL . Cambridge AR Research (The Automated Reasoning Group). 2017年3月5日時点のオリジナルよりアーカイブ。 2016年4月28日閲覧。
  4. ^ Jasmin Christian Blanchette、Lukas Bulwahn、Tobias Nipkow、「Isabelle/HOL における自動証明と証明」Archived 2021-10-15 at the Wayback Machine、Cesare Tinelli、Viorica Sofronie-Stokkermans (eds.)、 International Symposium on Frontiers of Combining Systems – FroCoS 2011、Springer、2011。
  5. ^ a b c Jasmin Christian Blanchette、Mathias Fleury、Peter Lammich、Christoph Weidenbach、「学習、忘却、再開、増分性を備えた検証済みSATソルバーフレームワーク」、Journal of Automated Reasoning 61 :333–365 (2018)。
  6. ^ Andrew Reynolds、Jasmin Christian Blanchette、Simon Cruanes、Cesare Tinelli、「SMT における再帰関数のモデル検索」、Nicola Olivetti、Ashish Tiwari（編）、第 8 回国際自動推論合同会議、Springer、2016 年。
  7. ^マカリウス、ウェンゼル (2025 年 3 月 13 日)。「Isabelle/Isar リファレンス マニュアル」(PDF) 。2025 年 5 月 10 日に取得。148ページ：「戦術による恣意的な目標の絞り込みは有害であると考えられる」。7.3節「戦術：不適切な証明方法」（172～175ページ）も参照。
  8. ^エバール、マヌエル;クライン、ガーウィン。ニプコウ、トビアス。ラリー・ポールソン;ティーマン、ルネ。「正式な証拠のアーカイブ」。2019 年10 月 22 日に取得。
  9. ^ 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.
  10. ^ Strniša, Rok; Parkinson, Matthew (2011年2月7日). 「Lightweight Java」 . Archive of Formal Proofs (2011年2月版). ISSN 2150-914X . 2019年11月25日閲覧。 

さらに読む

「 https://en.wikipedia.org/w/index.php?title=Isabelle_(proof_assistant)&oldid=1333532791」より取得