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

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

目次


第1節 関係式と論理変数

第2節 定理と証明の形

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

 第4節 環境部notation,contructors

第5節  環境部残り部分

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


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第3節 コンピュータによるチェック −環境部vocabulary

 前節の「定理の例」を実際のMizarの言語で書きますと、その書き方や証明が正しいかどうかを、自動的にコンピュータによりチェックすることができます(Mizar のシステムは、Mizar言語の定義と、チェックプログラムからなる、いわゆるproof checkerあるいはVerifierと呼ばれるものです)。

 チェックはhttp://www.wakasato.org/mizar/ http://www.wakasato.org/mizar/s7.0.05m4.09.842/verifier2/

というページで誰でも自由に行えます。そこにはBasic Package, Extended Package と Complete Packageの3つがあり、またMizarのバージョンも選べるようになっています。

 初心者の場合、Extended Packageを選び、バージョンは特に選ばなくてもそのままでいいでしょう(最新のバージョン)。しかしこのCAIではバージョンver 7.0.05 を使っていますので、もし例文などをチェックしてみたいときはそのバージョンを選んでください。Extended Packageボタンを押すと、入力欄が3つありますが、適当な文字列を入れればログオンできます。

 前節の「定理の例」をいきなりコピーペイストして、submitボタンを押してもうまくいきません。次のような準備が必要です。

 (1)environ という語ではじまる「環境部」をまず書きます。環境部は

   environ
       vocabulary     ...;
       notation    ...;
       constructors ...;
       clusters .....;
       requirements .....;
       schemes ...;
       theorems  ...;

のように書きます。

 ここでvocabularyというのは、新しく導入された単語が格納されたファイル(VOCファイル)の名を書き連ねる部分です。例えば上に掲げた「定理の例」では ^2とか^3とかが新しい単語にあたります。それらがどのVOCファイルに含まれるのかは次のようにして知ることができます。

 WebでMizar言語で書かれた数学をチェックするためのホームページhttp://www.wakasato.org/mizar/

において、今度はcomplete packageを選んでlogonします。すると下の方に

 Execute Mizar-Command というチェックボックスと、Mizar-Commandという1行だけの入力欄があります。チェックボックスにチェックを付け、コマンド入力欄に

     findvoc ^2

と入力し(適当なファイル名を上の欄に入れておく)、一番下にあるsubmitボタンを押します。すると、下方のCommand Consoleという、比較的大きな窓に

−−−−−−−−−
FindVoc, Mizar Ver. 7.0.05 (Linux/FPC)
Copyright (c) 1990,2004 Association of Mizar Users
vocabulary: METRIC_1
OEmpty^2-to-zero 

vocabulary: MONOID_1
O.:^2  230

vocabulary: SQUARE_1
O^2  254

vocabulary: TOPREAL1
OR^2-unit_square 
−−−−−−−−−

と表示されます。

 この見方は、「 ^2を含むVOCファイルがMETRIC_1.VOC, MONOID_1.VOC, SQUARE_1.VOC そして TOPREAL1.VOC と4つある。最初の OEmpty^2-to-zero について言うと最初のO はこの単語が関数として使われている、ということでこれを除いて考える。Empty^2-to-zeroというのが導入された単語である。この場合、^2は単語に含まれてはいるが、^2そのものではない。SQUARE_1.VOCの中にある、O^2 254 というのがそれである。Oは除いて考えるが、番号254というのは演算順序の強さを表す。255が最強である(数字の付いていないものがあるが、それは64)。例えば*は数字がついていないので64.従って a^2*3 と書くとa^6でなく、(a^2)*3である。とにかく^2はSQUARE_1で導入された単語である。」ということが分かります。

 同様にして^3について調べると、POLYEQ_3.VOC の中にあることが分かります。

 ここでいくつか注意があります。

 (1) ^2,^3は単語としてSQUARE_1,POLYEQ_3で導入されたが、その意味(定義そのもの)はSQUARE_1.MIZやPOLYEQ_3.MIZでなされている。

 (2) 同じ単語を使いながら、他の意味を与えることができる。つまりVOCファイルは新しく作らずに以前作られたものを使い、定義だけ新しく与えることができる。すると混同がおきて混乱するように見える。実際おきることが皆無ではないのだが、単語の使い方で通常は区別できる。例えば b を文字列としたとき

   b^2 を文字列b を2回続けて、長さが2倍の文字列、と定義することもできる。例えば、

   ("012345")^2="012345012345"

と考えるのである。この場合b^2がbの2乗ではない、ということはbが数ではなく文字列であることから分かる。このように大抵の場合は、その単語を記述したVOCファイルと、それを定義したMIZファイルは同一の名前であるが、そうでない場合も有る。

 「環境部」におけるvocabulary の後には、これから使用する単語が記述されます(VOCファイルをカンマで区切って列挙する。拡張子.VOCは付けない)。