多義語：proof -- 証明

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。

1. 辞書的意味
2. Isar文書内で、theoremコマンドによるIsar文の後に続く部分
3. 証明スクリプトとして記述された手順
4. 証明ドキュメントとして記述された宣言
5. 証明オブジェクト
6. 証明図 証明オブジェクトの一種と考えられる
7. 証明項 証明オブジェクトの一種と考えられる
8. 証明仮想マシン／抽象マシンの実行（run, execution）
9. 証明オブジェクトを作成するために、ユーザーと証明支援系が協力して行う行為。出来るだけ「リーズニング」と呼ぶことにする。

Isabelleは、論理式をシャローエンコーディングする（Shallow encoding - 檜山正幸のキマイラ飼育記 メモ編）ので、項としての証明オブジェクトはない。つまり、ポールソンのMに対する実装であるPure内部に証明を持つことは出来ない。

よって、証明を実体的に（システム内部のentityとして）定義するのは難しい。どうしても「書かれた手順」「書かれた宣言」のような話になる。