Mizar

読み方、または別称:みざーる

Mizar(ミザー、もしくはミザール)は自動証明検証システムで、数学的な証明を書くデータ記述言語とその言語で書かれた証明の内容を検証することができるプログラム、およびプログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理でできているライブラリで構成される。

Mizar言語で書かれたMizar論文はASCIIコードで書かれている。Mizar言語は、数学の通常の言葉使いと書式が類似している。また、証明を自動的に検証が可能なように形式化されたものである。

Mizar論文での証明の各段階は明白でなければならず、そのため同等の内容を持つ通常の数学論文に比べると4倍程度の長さになる。

Mizar の証明検証プログラムは Pascal で書かれており、古典論理を用いた証明を行うもので、商用以外の目的であればフリーでダウンロードして利用することができる。なお、PC/AT互換機の Windows, Solaris, FreeBSD および Linuxあるいは Mac OS X/Darwin で作動する。

ページトップへ戻る

話題の用語~今ホットな用語をご紹介

ITと社会用語辞典

ワークロード

ワークロードとは、システムのパフォーマンスを適正な状態に保つための指標のこと。

インターネット用語辞典

ライフログ

ライフログとは、人間の活動の記録(行動履歴)をデジタルデータとして記録すること、およびその記録のことである。

ページトップへ戻る