情報科学 の Mizarに関する解説。

株式会社 日立ソリューションズ

HITACHI Inspire the Next

  • ホーム
  • ソリューション・商品
  • 事例紹介
  • セミナー・展示会
  • ビジネスコラム
  • 企業情報
  • お問い合わせ

Mizar

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

Mizar(ミザー、もしくはミザール)は自動証明検証システムで、数学的な証明を書くデータ記述言語とその言語で書かれた証明の内容を検証することができるプログラム、およびプログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理でできているライブラリで構成される。
Mizar言語で書かれたMizar論文はASCIIコードで書かれている。Mizar言語は、数学の通常の言葉使いと書式が類似している。また、証明を自動的に検証が可能なように形式化されたものである。
Mizar論文での証明の各段階は明白でなければならず、そのため同等の内容を持つ通常の数学論文に比べると4倍程度の長さになる。
Mizar の証明検証プログラムは Pascal で書かれており、古典論理を用いた証明を行うもので、商用以外の目的であればフリーでダウンロードして利用することができる。なお、PC/AT互換機の Windows, Solaris, FreeBSD および Linuxあるいは Mac OS X/Darwin で作動する。

ページトップへ戻る

話題の用語

ITと社会用語辞典

ワークロード

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

インターネット用語辞典

ライフログ

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

ページトップへ戻る

情報漏洩防止ソリューション 「秘文」

ITのお悩みをソリュっと解決! 特命課ソリュートくんがいく!

『オムニチャネル』から商品を探すページです。日立ソリューションズは、コンサルティングからシステム構築、サポートとトータルソリューションをご提供するシステムインテグレーション企業です。

ページトップへ戻る