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

第4節 環境部notation,contructors

目次


第1節 関係式と論理変数

第2節 定理と証明の形

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

 第4節 環境部notation,contructors

第5節  環境部残り部分

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


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第4節 環境部notation,contructors

 環境部のnotation の部分に書くのは、本体部で使う単語の意味が定義されたMIZファイルの列挙です(拡張子.MIZは付けない)。そのファイルをどのようにして探すか、ということですが、VOCファイルと同じ名のMIZファイルを探すのが妥当です。しかしもしそれが違う意味であったのなら、次のページで探すのがいいでしょう。

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

ここからこれから自分が書こうとしている数学に一番近いファイル(.ABS という拡張子のファイル、abstructファイル)を探します。例えば実数に関するものならREAL_1,複素数に関するものならCOMPLEX1,COMPLEX2など。 そして自分の使いたい単語(記号、用語)が使われている部分を探します。見つかったらその上をクリックします。各単語にはリンクが張られています。従って、ページやラインのジャンプがあり、その単語の意味が最初に定義されている部分が表示されます。このようにしてその単語なり記号なり用語がどこで定義されたかを知ることができるのです。

 しかしその単語がどこで使われているかも分からないときは、次のページ

http://markun.cs.shinshu-u.ac.jp/Mirror/search_mml.html

を利用します。ここで使われている部分の検索ができます。

 以上述べたような便利なページへのリンク一覧は

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html

にあります。

 その単語が最初に使われているファイルが見つかったらそれを環境部の notation の後に書きます。

 これでチェックのためのページ

http://www.wakasato.org/mizar/

で、できかけの自分のファイルをチェックします。もしnotation の後に書いたファイルについて「 ::> 830: Nothing imported from notations (notaionから取りこむものが無い)」という意味のエラーが出るようなら、環境部のconstructors の後にもそのファイルの名前を付け足します。

 constructors に含めるファイルは、大雑把に言って複雑な定義がされているファイルです。そのようなときはnotationだけでなくconstructorsにもそのファイル名を書くのです。