|
|
情報証明論 第１章 論理式と証明の構造第６節 実際のチェック実行 |
|
目次
第１節 関係式と論理変数 第３節 コンピュータによるチェック −環境部vocabulary 第６節 実際のチェック実行
|
例のチェックのページ http://www.wakasato.org/mizar/ でＢａｓｉｃ Ｐａｃｋａｇｅを選び、定理を入力してみます。但し環境部としてSQUARE_1と同じものを書きます。そしてnotationとconstructorsにSQUARE_1そのものを加えておきます。更にPOLYEQ_3をvocabulary,notationに加えます。 また、本文の前に begin を付けておきます。
environ
vocabulary ARYTM, ARYTM_3, RELAT_1, ARYTM_1, ABSVALUE, SQUARE_1, XCMPLX_0,
COMPLEX1,POLYEQ_3;
notation TARSKI, SUBSET_1, ORDINAL1,NUMBERS,XCMPLX_0,XREAL_0,ABSVALUE,
SQUARE_1,POLYEQ_3;
constructors REAL_1, ABSVALUE, XCMPLX_0, XREAL_0, XBOOLE_0,SQUARE_1,POLYEQ_3;
clusters XREAL_0, REAL_1, NUMBERS, ARYTM_3, ZFMISC_1, XBOOLE_0, XCMPLX_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, REAL_1, XREAL_0;
theorems AXIOMS, REAL_1, ABSVALUE, XREAL_0, XCMPLX_0, XCMPLX_1;
begin
reserve x for Element of COMPLEX;
theorem (x^2 = 1 implies x=1 or x=-1) implies
(x^3 = 1 & x^2 =1 implies x=1 or x=-1)
proof assume A1: (x^2 = 1 implies x=1 or x=-1);
thus x^3 = 1 & x^2 =1 implies x=1 or x=-1
proof assume x^3 = 1 & x^2 =1;
hence x=1 or x=-1 by A1;
end;
end;
ここで reserve x for Element of COMPLEX というのは、変数x の型が、複素数型であることの宣言です。Ｍｉｚａｒ言語では（多くのプログラム言語と同じく）各変数に型（ｔｙｐｅ、 Ｍｉｚａｒではｍｏｄｅという）があります（複素数型にはElement of COMPLEXとcomplex numberと２つあります。本質的には同じなのですが、complex number ならば Element of COMPLEX は無条件では出ません。逆はいつでもいえます）。 x^3 は POLYEQ_3 において複素数について定義されており、x^2 もSQUARE_1 において複素数に対して拡張定義されているので、xの型を複素数型としたのです。
上の状態でＳｕｂｍｉｔボタンを押しますと ::> 830: Nothing imported from notations というエラー表示がnotation 部のPOLYEQ_3 の所に出ます。従ってconstructors の所へもPOLYEQ_3を加えてチェックをやり直してください。 すると多分エラーは無いはずです。エラーがあれば本文中にコメントの形（ :: をつけると行のそれ以後、改行までの文字列行がコメントになる ）でエラー番号が入ります。その意味は本文中の最後の方に、やはりコメントの形で表示されます。またError Informationのところにもエラーが表示されます。もしエラーが無ければ何も表示されません。 なお何度かチェックするとき、前のエラー番号が本文中に入ったまま、必要箇所を修正して、次のチェックをしてかまいません。システムは自動的に前のエラーコメントは消して、次のエラーコメントを（あれば）入れてくれます。
|