目次

まえがき
改訂版にあたって


1 Mizarの概要

2 Mizar言語の概要

3 Mizar articleの構成
3.1 全体構成
3.2 環境部
3.2.1 vocabulary部
3.2.2 notation部,constructors部
3.2.3 requirements部
3.2.4 definitions部
3.2.5 theorems部
3.2.6 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 の使い方
4.10 新しい変数の導入 (Set, reconsider)
4.11 take について
4.12 hereby

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 equqls の定義
6.6 mode の定義
6.7 Cluster の定義
6.8 structure の導入

7 実行環境
7.1 インストール
7.1.1 MS-DOS版
7.1.2 Linux版
7.2 Mizar を使うための準備
7.3 Mizar のシステム
7.4 Mizar の使い方
7.4.1 accommodate
7.4.2 Mizar チェッカー
7.4.3 エラーがある場合
7.4.4 便利なコマンド

8 ライブラリへの登録
8.1 article の改良
8.1.1 本体部の改良
8.1.2 環境部のチェック
8.2 登録の準備

9 便利なツール
9.1 用語のあるVOCファイルを探す (findvoc)
9.2 VOCファイルの中味を知る
9.3 その用語が使用されているABSファイルを知る
9.3.1 grep を使う方法
9.3.2 Webから検索する方法

10 バージョンアップについて

A 予約語一覧

B Mizar ライブラリ定理集
B.1 TARSKI
B.2 AXIOMS
B.3 BOOLE
B.4 XBOOL_0
B.5 XBOOL_1
B.6 REAL_1
B.7 NAT_1
B.8 FUNCT_1
B.9 SUBSET_1
B.10 FINSEQ_1
B.11 FUNCT_2
B.12 SQUARE_1
B.13 REAL_2

C C.1 Mizar Society 連絡先
C.1.1 Mizar Society
C.1.2 Mizar Society Nagano Circle
C.2 ftp による Mizar の入手法
C.3 インターネットの投稿法
C.4 WWW Homepage
C.5 Formalized Mathematics

あとがき
参考文献