Isabelle Tutorial その1 - caeruiro1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。 theory T imports B1, ..., Bn begin 宣言、定義、証明などなど end B1, ..., Bnは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。 既存の理論ファイルは次のページで探すことができますし、Isabelleをインストー
