definition let y be XFinSequence of INT,n be Integer; assume A1: 0< n & n< len a; switch(x) { case 1: break; case 2: break; default: } L:(x=1 or x=2 or not(x=1 & x=2)) now per cases by L; case LA:x=1; case LB:x=2; case LC:not (x=1 & x=2); end; C言語で処理 int sumarray_prg(int a[MAX_N],int n) { int s[MAX_N],i; if (!(0< n && n< MAX_N))return -1; s[0]=0; for (i=0;i< n;i++) { s[i+1]= s [i] + a[i+1]; } retu
このページ「Mizar」は、まだ書きかけです。加筆・訂正など、協力いただける皆様の編集を心からお待ちしております。また、ご意見などがありましたら、お気軽にトークページへどうぞ。
Mizar講義録(改訂第二版, HTML) Mizar講義録(改訂第四版, HTML) , PDF, MS-word Mizar 証明の構成法 (Skeletons of Mizar Proofs: Artur Korniłowicz 教授著) Hands-on tutorials Mizarの全ライブラリ (main site) (Josef Urban教授作成) "proof"が表示されている部分をクリックすると証明が閲覧可能! Mizarの全ライブラリ (another site) (Josef Urban教授作成) MML Content by Articles Mizarの記号辞書 : 従来の数学記号とMizarの記号の対照表 MML Reference search (by Dr. Kazuhisa Nakasho) MML 高機能検索システム (Grzegorz Bancer
Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqやIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。 内容： インストール 使ってみる 感想 インストール Mizarのオフィシャルサイトは： http://mizar.org/ 信州大学の日本語ページもあります。 http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html 信州大学のアーカイブから、自分の環境に応じたバイナリをダウンロードします。 ftp://markun.cs.shinshu-u.ac.jp/pub/mizar/system/current/ （バイナリの一覧） Windowsの場合、現時点（2016年12月）ではmizar-8
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
