Loading article…
Isabelle [ a ]自動定理証明器は、 Standard MLとScalaで記述された高階論理 (HOL) 定理証明器です。計算可能関数のための論理(LCF) スタイルの定理証明器として、明示的な証明オブジェクトを必要とせずに、かつそれをサポートすることで証明の信頼性を高めるために、小さな論理コア (カーネル) に基づいています。
Isabelleは、論理的に安全な拡張を可能にする柔軟なシステムフレームワーク内で利用可能であり、コード生成、ドキュメント作成、およびさまざまな形式手法の特定のサポートのための理論と実装の両方を含んでいます。これは、形式手法のための統合開発環境（IDE）と見なすことができます。近年、多数の理論とシステム拡張がIsabelle形式証明アーカイブ（Isabelle AFP）に収集されています。[ 2 ]
イザベルは、ローレンス・ポールソンがジェラール・ユエの娘にちなんで名付けた。 [ 3 ]
Isabelle定理証明器は、改訂版BSDライセンスの下でリリースされたフリーソフトウェアです。
Isabelleは汎用的な言語であり、メタ論理（弱い型理論）を提供し、一階述語論理（FOL）、高階述語論理（HOL）、ツェルメロ・フレンケル集合論（ZFC）などの対象論理を符号化するために使用されます。最も広く使用されている対象論理はIsabelle/HOLですが、重要な集合論の発展はIsabelle/ZFで行われました。Isabelleの主な証明方法は、高階単一化に基づく、分解の高階版です。
Isabelleは対話型ではあるものの、項書き換えエンジンやタブロー証明器などの効率的な自動推論ツール、さまざまな決定手順、そしてSledgehammer証明自動化インターフェースを介して外部充足可能性法理論（SMT）ソルバー（CVC4を含む）や、 E、SPASS、Vampireなどの分解ベースの自動定理証明器（ATP）を備えています（Metis [ b ]証明法は、これらのATPによって生成された分解証明を再構築します）。[ 4 ]また、 Nitpick [ 5 ]とNunchaku [ 6 ]という2つのモデルファインダー（反例生成器）も備えています。
Isabelleには、大規模な証明を構造化するモジュールであるロケールがあります。ロケールは、指定されたスコープ内で型、定数、仮定を固定します[ 5 ] 。これにより、すべての補題に対してそれらを繰り返す必要がなくなります。
Isar（「理解可能な半自動推論」）は、Isabelleの形式的証明言語です。これはMizarシステムに触発されています。[ 5 ]
Isabelleでは、証明を手続き型と宣言型の2つの異なるスタイルで記述できます。手続き型証明では、適用する一連の戦術（定理証明関数/手順）を指定します。これは、人間の数学者が結果を証明するために適用する手順を反映していますが、これらの手順の結果を記述しないため、通常は読みにくいです。このスタイルは、Isabelleのドキュメントでは「有害」とみなされています。[ 7 ]
一方、宣言型証明（Isabelleの証明言語であるIsarでサポートされている）は、実際に実行される数学的演算を指定するため、人間にとって読みやすく、検証しやすい。
例えば、イサールにおける背理法による「 2の平方根は有理数ではない」という宣言的証明は、次のように記述できる。
定理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により、"2 * n^2 = 2^2 * k^2"はsimp により、したがって"2 dvd n^2"はsimp により、したがって"2 dvd n"はsimp により、qed ‹2 dvd m›は"2 dvd gcd m n"を持ち、 (rule gcd_greatest) により、 lowest_termsにより"2 dvd 1"を持ち、したがってFalse であり、 odd_one はblast により、 qed となります。
Isabelleは、ソフトウェアおよびハードウェアシステムの仕様策定、開発、検証のための形式手法を支援するために使用されてきました。
Isabelleは、ゲーデルの完全性定理、選択公理の無矛盾性に関するゲーデルの定理、素数定理、セキュリティプロトコルの正当性、プログラミング言語のセマンティクスの特性など、数学やコンピュータサイエンスの数多くの定理を形式化するために使用されてきました。前述のように、形式的証明の多くは形式的証明アーカイブに保管されており、そこには（2019年現在）少なくとも500の記事があり、合計で200万行を超える証明が含まれています。[ 8 ]
いくつかの言語やシステムで同様の機能が提供されています。