7. Inductively Defined Setsこの章では集合の帰納的定義を紹介します。 7.1 The Set of Even Numbers 偶数の集合は、定数0と演算子+2からなる最小の集合として帰納的に定義できます。もちろん、整除関係(dvd)を使用しても定義できます。それぞれの方法で定…

6.6 Case Study: Verified Model Checking ケーススタディとしてComputation Tree Logic(CTL)を使ったモデル検査を取り上げます。モデル検査の基礎は集合論であり、これをHOLを使って見てみます。まずpropositional dynamic logic(PDL)と呼ばれる単純な様相…

6.4 Well-Founded Relations and Induction 整礎性は手続きの停止性と関係します。例えば複雑な再帰関数の定義にはその停止性を保証するための整礎関係を示す必要があり、また多くの数学的帰納法は整礎帰納法の特別な場合です。関係が整礎であるとは、関係が…

6. Sets, Functions and Relationsこの章では集合、関数、関係を見ていきます。集合は、例えば言語理論や計算理論、状態遷移機械など計算機科学における形式化にも有用です。Isabelleは、集合計算が含まれる多くの式も自動証明します。このドキュメントで全…

5.17 Managing Large Proof 長くなりがちな証明のステップを短くする方法を見ていきます。 5.17.1 Tacticals, or Control Structures 長い証明の中には、規則性が現れることがあります。プラス記号(+)を使用して、ステップを繰り返すことができます。例えば…

5.15 Forward Proof: Transforming Theorems ここまでは後ろ向きの証明を扱ってきましたが、前向きに証明を行うこともできます。前向きの証明は、一般的な定理から固有の定理を導くのに便利です。例えば最大公約数の分配法則を考えます。 k * gcd(m, n) = gc…

5.12 Proving Theorems Using the blast Method Isabelleのclassical reasonerは自動証明のためのツールの一つであり、その中でも最も重要なメソッドがblastです。述語論理の例から見ていきます。次の例はAndrew's challengeと呼ばれ、自動証明が難しいとさ…

5.10 Description Operators HOLには二つの記述演算子があります。確定記述はその式を満たす唯一の値を表わします。不確定記述はその式を満たす任意の値を表わします。 5.10.1 Definite Description 確定記述は伝統的にιx. P(x)と書きます。これは、P(x)を満…

5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。メソッドeruleはQとサブゴールを単一化する…

5. The Rules of the Gameこの章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。 5.1 Natural Deducation Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。 Isabelleでは自然演繹を使…