コンテンツにスキップ

Mizar/構文

出典: フリー教科書『ウィキブックス(Wikibooks)』

書き方

集合論から全ての証明を行っているので、『A→B』 の証明をするには、以下の書き方をする
environ

begin
 for A,B being set st A holds B
proof
 let A,B be set;
 assume A1: A;
 thus B by A1;
end;
証明のトートロジーより『A→B』と同値なものとして、『¬A∨B』が得られる。

この処理系では正しいことを『1』、正しくないことを『0』とします。 従って、処理系の内部では、上記の処理は以下の処理のように取り扱われる。

{A,B⊂集合|A→B}
証明
 A,B⊂集合
 ¬A ∨ B

型と書式の確認をした後で、

A=1,B=1;
not(A) and B;

の処理を行い。

0 and 1

の結果は

1

となり、正しいということになる。 だから、『assume』は英訳では仮定なのだが、Mizarの処理系では『not』となり、 『thus ~ by ラベル』 は 『ラベル and ~ 』となる。