|
自動証明検証システム Mizar（ミザー、ミザール）は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語（-言語）、実際にその言語で記述された証明の内容を検証することができる計算機プログラム（証明検証プログラム）、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ () の三者から構成される。 と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。 と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。 == 概要 == システムの開発は1973年にアンジェイ・トリブレッツによって始められ、システムの保守をポーランドの、カナダのアルバータ大学、日本の信州大学で行っている。 -言語で記された証明文（以下、-論文）は普通のASCIIコードで書かれている。-言語は、数学の通常の言葉遣いと書式がよく似ており、数学者ならば-論文を容易に読むことができる。また、証明を自動的に検証可能とするほど十分に形式化されたものである。-論文における証明の各段階は非常に自明なものである必要があり、そのため同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された。 の証明検証プログラムはPascalでかかれ、古典論理を用いた証明を行うもので、非商用目的であれば無料でダウンロード、利用が可能である。これはPC/AT互換機上のWindows、Solaris、FreeBSDおよびLinuxで、あるいはMac OS X / Darwinで動く。ソースコードは-ユーザ協会〔〕のメンバーだけが入手できる。 の配布物には、新たに書かれる -論文で参照可能な種々の定義および定理から成る数学ライブラリが含まれる。レビューと自動検証を受けた新たな論文は、形式化数学ジャーナル〔〕の関連刊行物で公表することができ、また然る後の一部に組み込まれる。 はタルスキー・グロタンディーク集合論の公理に基づいて構築される。2008年5月現在、8,800の定義と46,000の定理を含む〔最新の統計についてはを見よ〕。例えばハーン・バナッハの定理、ケーニヒの補題、ブラウワーの不動点定理、ゲーデルの完全性定理、カントール集合に関するいくつかの事実、などがに含まれる。 の扱う全ての対象は意味論的には集合であるけれども、にも拘らず-言語では統語論的な「型」を定義して使うことが許されている。つまり、ある変数がたとえば自然数を表すものならば Nat-型を、あるいは群を表すならGroup-型を宣言することができる。このような記法は数学者にとっての記号の捉え方とより近く、-言語をより扱いやすいものにしている。閲覧可能な-論文の概要は形式化数学ジャーナルのウェブサイト〔から入手できる。また〔〕は-検索エンジンを実装している。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Mizar」の詳細全文を読む スポンサード リンク
|