Chapter 8

ライブラリへの登録

Mizar ライブラリへの登録について説明します．Mizar の article を書いて，チェッカーを通ったとします．しかし，チェッカーを通っただけでは，Mizarライブラリに登録することはできません．登録する前にいくつかやることがあります．

8.1 articleの改良

8.1.1 本体部の改良

まず，article の改良をしなければなりません．このためのコマンドとしては，

RELPREM 余計な引用をチェックする．

CHKLAB 　余計なラベルをチェックする．

INACC 余計な行をチェックする．

TRIVDEMO トリビアルな証明をチェックする．

というコマンドが用意されています．いずれのコマンドも，

RELPREM TEXT＼EXAMPLE1.MIZ

のように使い，それぞれのコマンドを実行した後に，

ERRFLAG TEXT＼EXAMPLE1.MIZ

を実行すると，先程と同様に，article にエラー番号が書きこまれます．

RELPREM は，by の後ろに推論に関係ないものが引用されているかをチェックします．また，then についても，それが必要であるかどうかチェックします．もし，それがなくても推論できるようなものがあると，エラーになります．

CHKLAB は，ラベルをつけたが，あとで使ってないラベルをチェックします．

INACC は，あとで引用されてない行をチェックします．もし，このチェックでエラーがでて，行を削除した場合，それにより余計な引用やラベルができるかもしれませんので，また最初からチェックしなければいけません．

TRIVDEMO は，トリビアルな証明があるかどうかチェックします．トリビアルなものは取り除かなくてはなりません．

これらが，本体部のチェックです．

8.1.2 環境部のチェック

そのほか環境部のチェックがあります．このためのコマンドとしては，



IRRVOC   不要な  vocabulary をチェックする．



IRRDEF(Mizar version 4.09 ではありません.)



         不要な  definition をチェックする ．
 


IRRTHS   不要な theorems をチェックする．

があります．使い方は本体部のチェックのコマンドと同様です．signature に関しては，良い方法がないということで，今の時点では, IRRSIG というのは出来ていません．ですから，signature は最初からたくさん使わないで，なるべく最低限のもの，最初は0から出発して，だんだん自分に必要なものを入れていってください，ということです．

それから signature に関しては，順序が重要になることがあります．なるべく速い時期に作られたものから引用したほうがいいということです．abstract file を参照して，だいたい順序どうりに入れるということが重要になります．