情報証明論 第1章 論理式と証明の構造

第5節  環境部残り部分

目次


第1節 関係式と論理変数

第2節 定理と証明の形

第3節 コンピュータによるチェック −環境部vocabulary

 第4節 環境部notation,contructors

第5節  環境部残り部分

   第6節 実際のチェック実行


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第5節  環境部残り部分

 実際に証明をチェックのためのページに入力してチェックしてみましょう。

 環境部ですが、前節で述べた通りなのですが、実際には自分が書こうとしているものに近いファイルを探し、そのMIZファイルから環境部をそっくりコピーするといいでしょう。後で余分なファイルを環境部から除去することができますので、多めに加えておいていいのです。

 また2つ以上のファイルに関連した数学を書きたいならば、それらの環境部を寄せ集めればいいでしょう。

 例えば前々節で紹介したようなa^2とa^3に関するようなものを書きたい場合、

SQUARE_1.MIZ と POLYEQ_3.MIZ にある環境部を合併させればいいのです。

       clusters .....;
       requirements .....;
       schemes ...;
       theorems  ...;

の各部についても機械的に合併すればいいのです。しかし一応それらを説明しておきますと、theorems は証明の際に引用する定理や定義のあるファイルの名前を書きます。... by SQUARE_1:12;

などと引用するのですが、この場合のby の後に来るファイル名を書くのです。

 clustersはcluster という複合語(例えば non negative Real といったようなもの。ASYMPT_0 にclusterとして定義されている)が定義されているファイルを書くところです。

 requirements はチェッカーに計算能力を与えるためのファイル名を書きます。だいたい書くファイルは決まっています。ARITHM, SUBSET, REAL, BOOLE, NUMERALSなどです。

 ARITHMは複素数(または実数)xについて

x + 0 = x, x * 0 = 0, 1 * x = x, x - 0 = x,0 / x = 0, x / 1 = x

といった式の変形を理由(引用)なしに行えるようにするもの。

 SUBSETとBOOLEは集合論に関するもの。REALは実数に関するもの、NUMERALSは自然数に関するものです。

 schemesの後に書くのは、schemeという特別の定理があるファイルを書きます。例えば数学的帰納法などは通常の定理では記述できない(1階の述語論理で記述できない)ので、schemeという一種の拡張定理を使います。これを引用するときは by ...と書かず、 from ... と書きます。

 Mizar言語については解説書が少ない、とよく言われますが、過去のファイルが何百何千とあり、それらはWebで容易に見ることができますので、それらを参考にすればいいのです。

 なおabstructファイルはMIZファイルから証明を除いて、ラベルを整理した要約版です。それは

 http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/mmlident.html

に公開されている、ということを書きましたが、そこから関連するファイルをクリックするとページの上の方に

Mizar article,  

というリンクがあります。これがMIZファイルへのリンクです。そこにはそのファイル中の全命題の完全な証明が載っているのです。