Mizar

出典: フリー百科事典『ウィキペディア（Wikipedia）』

自動証明検証システム Mizar（ミザー、ミザール）は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのプログラミング言語（Mizar 言語）、実際にその言語で記述された証明の内容を検証することができる計算機プログラム（証明検証プログラム）、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ（MML）の三者から構成される。

システムの開発は1973年にアンジェイ・トリブレッツによって始められ、システムの保守をポーランドのビャウィストク大学 (en:Białystok University)、カナダのアルバータ大学、日本の信州大学で行っている。

Mizar 言語で記された証明文（以下、Mizar 論文）は普通のASCIIコードで書かれている。Mizar 言語は、数学者ならばすんなり Mizar 論文を読んで理解することが可能であるほどに数学用語に似通ったものであり、また証明が自動的に検証可能なほどに形式的なものである。Mizar 論文における証明の各段階は非常に自明なものである必要があり、同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された。

Mizar の証明検証プログラムは Pascal でかかれ、古典論理を用いた証明を行うもので、非商用目的であれば無料でダウンロード、利用が可能である。これはPC/AT互換機上のWindows、Solaris、FreeBSDおよびLinuxで、またMac OS X/Darwinで動く。ソースコードは Association of Mizar Users のメンバーだけが入手できる。

Mizar の配布物には、新たに書かれる Mizar 論文で参照可能な種々の定義および定理から成る Mizar 数学ライブラリ (Mizar Mathematical Library, MML) が含まれる。レビューと自動検証を受けた新たな論文は、形式化数学 (Formalized Mathematics) の関連刊行物で公表することができ、また然る後 MML の一部に組み込まれる。

MML はタルスキー・グロタンディーク集合論の公理に基づいて構築される。2005年現在、8,000の定義と40,000の定理を含む（最新の統計については[1]を見よ）。例えばハーン・バナッハの定理(en:Hahn-Banach_theorem)、ケーニヒの補題(en:König's_lemma)、ブラウワーの不動点定理(en:Brouwer_fixed_point_theorem)、ゲーデルの完全性定理(en:Gödel's_completeness_theorem)、カントール集合に関するいくつかの事実、などが MML に含まれる。

意味論的には MML の扱う全ての対象は集合であるけれども、にも拘らず Mizar 言語は構文型を定義して使うことが許されている。つまり、ある変数がたとえば自然数を表すものならば Nat 型を、あるいは群を表すなら Group 型を宣言することができる。これにより、Mizar 記法はより使いやすく、また数学者の記号の使い方により近いものになる。

閲覧可能な MML 論文の概要は Journal of Formalized Mathematics から入手できる。また MML Query は MML 検索エンジンを実装している。

[編集] 外部リンク

• Main Mizar site - MML、Formalized Mathematics の刊行物へのリンクと、いくつかのシステムの入門書へリンクする参考文献一覧の項
• MML Query - MMLの検索エンジン
• Freek Wiedijk's Mizar site - このシステムについて話されたカンファレンスについてのスライドと40ページの入門的な論文
• Association of Mizar Users
• A paper about Mizar history
• マークンベア