Chapter 1

Mizarの概要

Mizar とは，ワルシャワ大学(ポーランド)の Andrzej Trybulec 先生を中心とした Mizar Society によってすすめられている，数学をコンピュータを使って形式化するプロジェクトの総称です． Mizar プロジェクトは，コンピュータを使って数学を記述するために作られた Mizar 言語によって数学の証明を記述し，それを IBM-PC 上で動作する Mizar プルーフチェッカーによってチェックし，それを Mizar ライブラリに登録することによって行われます．このプロジェクトの目的は数学の論文のチェックのシステムを作ることです． Mizar では，数学の証明を記述したテキストのことを article といいます．新たに article を書くときには，すでにチェックされていて Mizar ライブラリに登録されている多くの article を参照することができます．そして，その article がいずれ Mizar ライブラリに登録されたときには，それを他の article が参照することもできます．
　article は，環境部 (environ)，本体部 (textproper) に分かれており，環境部では，その article に必要な様々な環境設定を記述し，本体部では証明自体を記述します．
　article は Mizar 言語によって記述します． Mizar 言語は，数学の一般的な証明の記述のしかたをもとにしていますが， Mizar 独特の書き方もあり，これについては後で詳しく説明します．
　ここでは Mizar 言語，Mizar プルーフチェッカー，さらに Mizar プロジェクトについて説明します．