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

Mizar と同様の目的を持つプロジェクトに、ロバート・ボイヤーQEDプロジェクトがある。

概要

編集

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

Mizar-言語で記された証明文(以下、Mizar-論文)は普通のASCIIコードで書かれている。Mizar-言語は、数学の通常の言葉遣いと書式がよく似ており、数学者ならばMizar-論文を容易に読むことができる。また、証明を自動的に検証可能とするほど十分に形式化されたものである。Mizar-論文における証明の各段階は非常に自明なものである必要があり、そのため同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された。

Mizarの証明検証プログラムはPascalでかかれ、古典論理を用いた証明を行うもので、非商用目的であれば無料でダウンロード、利用が可能である。これはPC/AT互換機上のWindowsSolarisFreeBSDおよびLinuxで、あるいはmacOS / Darwinで動く。ソースコードはMizar -ユーザ協会[1]のメンバーだけが入手できる。

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

MMLタルスキー・グロタンディーク集合論の公理に基づいて構築される。2008年5月現在、8,800の定義と46,000の定理を含む[3]。例えばハーン・バナッハの定理ケーニヒの補題ブラウワーの不動点定理ゲーデルの完全性定理カントール集合に関するいくつかの事実、などがMMLに含まれる。

MMLの扱う全ての対象は意味論的には集合である一方、Mizar-言語では統語論的な「型」を定義して使うことが許されている。例えば、ある変数が自然数を表すものならばNat-型を、を表すならGroup-型を宣言することができる。このような記法は数学者にとっての記号の捉え方とより近く、Mizar-言語をより扱いやすいものにしている。

閲覧可能なMML-論文の概要は形式化数学ジャーナルのウェブサイト[2]から入手できる。またMML Query[4]MML-検索エンジンを実装している。

注記

編集
  1. ^ Association of Mizar Users
  2. ^ a b Journal of Formalized Mathematics
  3. ^ 最新の統計については[1]を見よ
  4. ^ MML Query

外部リンク

編集