Mizar4 フレーム版

<BODY> <P><FONT size="6">目次</FONT></P> <TABLE> <TBODY> <TR> <TD colspan="4"><A href="../ja/preface.html">まえがき</A></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="../ja/preface2.html">改訂版にあたって</A></TD> <TD></TD> </TR> <TR> <TD><BR> </TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>1</TD> <TD colspan="3"><A href="../ja/chapter1.html">Mizarの概要</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>2</TD> <TD colspan="3"><A href="../ja/chapter2.html">Mizar言語の概要</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>3</TD> <TD colspan="3"><A href="../ja/chapter3_1.html">Mizar articleの構成</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.1</TD> <TD colspan="2"><A href="../ja/chapter3_1.html">全体構成</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.2</TD> <TD colspan="2"><A href="../ja/chapter3_2.html">環境部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.1</TD> <TD><A href="../ja/chapter3_2_1.html">vocabulary部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.2</TD> <TD><A href="../ja/chapter3_2_2.html">notation部，constructions部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.3</TD> <TD><A href="../ja/chapter3_2_3.html">requirements部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.4</TD> <TD><A href="../ja/chapter3_2_4.html">definitions部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.5</TD> <TD><A href="../ja/chapter3_2_5.html">theorems部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.6</TD> <TD><A href="../ja/chapter3_2_6.html">schemes部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.3</TD> <TD colspan="2"><A href="../ja/chapter3_3_1.html">本体部</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.3.1</TD> <TD><A href="../ja/chapter3_3_1.html">文</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.3.2</TD> <TD><A href="../ja/chapter3_3_2.html">定理</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>4</TD> <TD colspan="3"><A href="../ja/chapter4_1.html">証明の方法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.1</TD> <TD colspan="2"><A href="../ja/chapter4_1.html">基本的な証明方法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.2</TD> <TD colspan="2"><A href="../ja/chapter4_2.html">背理法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.3</TD> <TD colspan="2"><A href="../ja/chapter4_3.html">証明の分割</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.4</TD> <TD colspan="2"><A href="../ja/chapter4_4.html">同値の証明</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.5</TD> <TD colspan="2"><A href="../ja/chapter4_5.html">now の使い方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.5.1</TD> <TD><A href="../ja/chapter4_5_1.html">end についての注意</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.6</TD> <TD colspan="2"><A href="../ja/chapter4_6.html">全称記号</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.1</TD> <TD><A href="../ja/chapter4_6_1.html">変数が2つある場合</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.2</TD> <TD><A href="../ja/chapter4_6_2.html">such that を使った書き方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.3</TD> <TD><A href="../ja/chapter4_6_3.html">文の分割</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.4</TD> <TD><A href="../ja/chapter4_6_4.html">文の分割 assume での場合</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.5</TD> <TD><A href="../ja/chapter4_6_5.html">that の後の注意</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.7</TD> <TD colspan="2"><A href="../ja/chapter4_7.html">存在記号</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.7.1</TD> <TD><A href="../ja/chapter4_7_1.html">consider の使い方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.7.2</TD> <TD><A href="../ja/chapter4_7_2.html">given の使い方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.8</TD> <TD colspan="2"><A href="../ja/chapter4_8.html">場合分け</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.1</TD> <TD><A href="../ja/chapter4_8_1.html">場合分けの前提</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.2</TD> <TD><A href="../ja/chapter4_8_2.html">場合わけでのラベル</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.3</TD> <TD><A href="../ja/chapter4_8_3.html">ラベルについての注意</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.9</TD> <TD colspan="2"><A href="../ja/chapter4_9.html">@proof の使い方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.10</TD> <TD colspan="2"><A href="../ja/chapter4_10.html">新しい変数の導入 (Set, reconsider)</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.11</TD> <TD colspan="2"><A href="../ja/chapter4_11.html">take について</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.12</TD> <TD colspan="2"><A href="../ja/chapter4_12.html">hereby</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>5</TD> <TD colspan="3"><A href="../ja/chapter5_1.html">mode について</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.1</TD> <TD colspan="2"><A href="../ja/chapter5_1.html">mode</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.2</TD> <TD colspan="2"><A href="../ja/chapter5_2.html">階層構造</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.3</TD> <TD colspan="2"><A href="../ja/chapter5_3.html">mode の変更</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.4</TD> <TD colspan="2"><A href="../ja/chapter5_4.html">証明中の mode の宣言</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>5.4.1</TD> <TD><A href="../ja/chapter5_4_1.html">c= についての注意</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>5.4.2</TD> <TD><A href="../ja/chapter5_4_2.html">実際に definition を使っている例</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>6</TD> <TD colspan="3"><A href="../ja/chapter6_1.html">定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.1</TD> <TD colspan="2"><A href="../ja/chapter6_1.html">定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.2</TD> <TD colspan="2"><A href="../ja/chapter6_2.html">vocabulary file の書き方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.3</TD> <TD colspan="2"><A href="../ja/chapter6_3.html">predicate の定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.4</TD> <TD colspan="2"><A href="../ja/chapter6_4.html">functor の定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.5</TD> <TD colspan="2"><A href="../ja/chapter6_5.html">equqls の定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.6</TD> <TD colspan="2"><A href="../ja/chapter6_6.html">mode の定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.7</TD> <TD colspan="2"><A href="../ja/chapter6_7.html">Cluster の定義</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.8</TD> <TD colspan="2"><A href="../ja/chapter6_8.html">structure の導入</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>7</TD> <TD colspan="3"><A href="../ja/chapter7.html">実行環境</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.1</TD> <TD colspan="2"><A href="../ja/chapter7_1_1.html">インストール</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.1.1</TD> <TD><A href="../ja/chapter7_1_1.html">MS-DOS版</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.1.2</TD> <TD><A href="../ja/chapter7_1_2.html">Linux版</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.2</TD> <TD colspan="2"><A href="../ja/chapter7_2.html">Mizar を使うための準備</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.3</TD> <TD colspan="2"><A href="../ja/chapter7_3.html">Mizar のシステム</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.4</TD> <TD colspan="2"><A href="../ja/chapter7_4_1.html">Mizar の使い方</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.1</TD> <TD><A href="../ja/chapter7_4_1.html">accommodate</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.2</TD> <TD><A href="../ja/chapter7_4_2.html">Mizar チェッカー</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.3</TD> <TD><A href="../ja/chapter7_4_3.html">エラーがある場合</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.4</TD> <TD><A href="../ja/chapter7_4_4.html">便利なコマンド</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>8</TD> <TD colspan="3"><A href="../ja/chapter8.html">ライブラリへの登録</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>8.1</TD> <TD colspan="2"><A href="../ja/chapter8_1_1.html">article の改良</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>8.1.1</TD> <TD><A href="../ja/chapter8_1_1.html">本体部の改良</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>8.1.2</TD> <TD><A href="../ja/chapter8_1_2.html">環境部のチェック</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>8.2</TD> <TD colspan="2"><A href="../ja/chapter8_2.html">登録の準備</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>9</TD> <TD colspan="3"><A href="../ja/chapter9_1.html">便利なツール</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.1</TD> <TD colspan="2"><A href="../ja/chapter9_1.html">用語のあるVOCファイルを探す (findvoc)</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.2</TD> <TD colspan="2"><A href="../ja/chapter9_2.html">VOCファイルの中味を知る</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.3</TD> <TD colspan="2"><A href="../ja/chapter9_3_1.html">その用語が使用されているABSファイルを知る</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>9.3.1</TD> <TD><A href="../ja/chapter9_3_1.html">grep を使う方法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>9.3.2</TD> <TD><A href="../ja/chapter9_3_2.html">Webから検索する方法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>10</TD> <TD colspan="3"><A href="../ja/chapter10.html">バージョンアップについて</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>A</TD> <TD colspan="3"><A href="../ja/appendix_A.html">予約語一覧</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>B</TD> <TD colspan="3"><A href="../ja/appendix_B.html">Mizar ライブラリ定理集</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.1</TD> <TD colspan="2"><A href="../ja/appendix_B_1.html">TARSKI</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.2</TD> <TD colspan="2"><A href="../ja/appendix_B_2.html">AXIOMS</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.3</TD> <TD colspan="2"><A href="../ja/appendix_B_3.html">BOOLE</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.4</TD> <TD colspan="2"><A href="../ja/appendix_B_4.html">XBOOL_0</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.5</TD> <TD colspan="2"><A href="../ja/appendix_B_5.html">XBOOL_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.6</TD> <TD colspan="2"><A href="../ja/appendix_B_6.html">REAL_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.7</TD> <TD colspan="2"><A href="../ja/appendix_B_7.html">NAT_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.8</TD> <TD colspan="2"><A href="../ja/appendix_B_8.html">FUNCT_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.9</TD> <TD colspan="2"><A href="../ja/appendix_B_9.html">SUBSET_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.10</TD> <TD colspan="2"><A href="../ja/appendix_B_10.html">FINSEQ_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.11</TD> <TD colspan="2"><A href="../ja/appendix_B_11.html">FUNCT_2</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.12</TD> <TD colspan="2"><A href="../ja/appendix_B_12.html">SQUARE_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.13</TD> <TD colspan="2"><A href="../ja/appendix_B_13.html">REAL_2</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>C</TD> <TD>C.1</TD> <TD colspan="2"><A href="../ja/appendix_C_1.html">Mizar Society 連絡先</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>C.1.1</TD> <TD><A href="../ja/appendix_C_1.html">Mizar Society</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>C.1.2</TD> <TD><A href="../ja/appendix_C_1.html">Mizar Society Nagano Circle</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.2</TD> <TD colspan="2"><A href="../ja/appendix_C_2.html">ftp による Mizar の入手法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.3</TD> <TD colspan="2"><A href="../ja/appendix_C_3.html">インターネットの投稿法</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.4</TD> <TD colspan="2"><A href="../ja/appendix_C_4.html">WWW Homepage</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.5</TD> <TD colspan="2"><A href="../ja/appendix_C_5.html">Formalized Mathematics</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="../ja/postface.html">あとがき</A></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="../ja/postface.html">参考文献</A></TD> <TD></TD> </TR> </TBODY> </TABLE> </BODY>