Mizar
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/10/19 08:16 UTC 版)
自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。
- ^ Association of Mizar Users
- ^ a b Journal of Formalized Mathematics
- ^ 最新の統計については[1]を見よ
- ^ MML Query
- 1 Mizarとは
- 2 Mizarの概要
- 3 外部リンク
- Mizarのページへのリンク