目次

１　Ｍｉｚａｒの概要

２　Ｍｉｚａｒ言語の概要

３　Ｍｉｚａｒ　ａｒｔｉｃｌｅの構成

            3．1　全体構成



            3．2　環境部



                    3．2．1　vocabulary　部



                    3．2．2　signature　部



                    3．2．3　definitions　部



                    3．2．4　theorems　部



                    3．2．5　schemes　部



             3．3　本体部



                    3．3．1　文



                    3．3．2　定理

4　証明の方法

              4．1　基本的な証明方法



              4．2　背理法



              4．3　証明の分割



              4．4　同値の証明



              4．5　nowの使い方



                     4．5．1　endについての注意



              4．6　全称記号



                     4．6．1　変数が2つある場合



                     4．6．2　such thatを使った書き方



                     4．6．3　文の分割



                     4．6．4　文の分割　assumeでの場合



                     4．6．5　thatの後の注意



               4．7　存在記号



                     4．7．1　considerの使い方



                     4．7．2　givenの使い方



               4．8　場合分け



                     4．8．1　場合分けの前提



                     4．8．2　場合分けでのラベル



                     4．8．3　ラベルについての注意



                4．9　@proof の使い方

5　modeについて

                 5．1　mode
 


                 5．2　階層構造



                 5．3　modeの拡張



                 5．4　証明中の mode の宣言
　


                      5．4．1　c=　についての注意



                      5．4．2　実際に definition を使っている例

6　定義

                  6．1　定義



                  6．2　vocabulary file の書き方



                  6．3　predicate の定義



                  6．4　functor の定義



                  6．5　mode の定義

7　実行環境

                   7．1　インストール



                   7．2　Mizar を使うための準備



                   7．3　Mizar のシステム



                   7．4　Mizar の使い方



                        7．4．1　accommodate



                        7．4．2　Mizar チェッカー



                        7．4．3　エラーがある場合



                        7．4．4　便利なコマンド



                        7．4．5　エデイターから Mizar を呼び出す方法

8　ライブラリへの登録

                   8．1　article の改良



                        8．1．1　本体部の改良



                        8．1．2　環境部のチェック



               　　 8．2　登録の準備

Ａ　予約語一覧表

                     Ａ.1　Mizar　チェッカー（アコモデータも含む）



                     Ａ．2　アコモデータのみ

Ｂ　Mizar　ライブラリ定理集

                      Ｂ.1　ＴＡＲＳＫＩ



                      Ｂ.2　ＡＸＩＯＭＳ



                      Ｂ.3　ＢＯＯＬＥ



                      Ｂ.4　ＲＥＡＬ＿1



                      Ｂ.5　ＮＡＴ＿1



                      Ｂ.6　ＦＵＮＣＴ＿1



                      Ｂ.7　ＳＵＢＳＥＴ＿1



                      Ｂ.8　ＦＩＮＳＥＱ＿1



                      Ｂ.9　ＦＵＮＣＴ＿2



                      Ｂ.10　ＡＮＡＬ＿1



                      Ｂ.11　ＳＱＵＡＲＥ＿1



                      Ｂ.12　ＲＥＡＬ＿2

アスキーコード表

アスキーコード表(2)

Appendix Ｄ

               Mizar　Society 連絡先



                               Ｄ．1．1　Mizar　Society



                               Ｄ．1．2　Mizar　Society　Nagano　Circle



          　　　Ｄ．2　ftp による Mizar の入手法



                       Ｄ.3　WWW Homepage



                       Ｄ.4  Formalized Mathematics


Back