情報証明論 第1章 論理式と証明の構造

第6節 実際のチェック実行

目次


第1節 関係式と論理変数

第2節 定理と証明の形

第3節 コンピュータによるチェック −環境部vocabulary

 第4節 環境部notation,contructors

第5節  環境部残り部分

   第6節 実際のチェック実行


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第6節 実際のチェック実行

 例のチェックのページ

 http://www.wakasato.org/mizar/

でBasic Packageを選び、定理を入力してみます。但し環境部として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 の型が、複素数型であることの宣言です。Mizar言語では(多くのプログラム言語と同じく)各変数に型(type、 Mizarではmodeという)があります(複素数型にはElement of COMPLEXとcomplex numberと2つあります。本質的には同じなのですが、complex number ならば Element of COMPLEX は無条件では出ません。逆はいつでもいえます)。

x^3 は POLYEQ_3 において複素数について定義されており、x^2 もSQUARE_1 において複素数に対して拡張定義されているので、xの型を複素数型としたのです。

 上の状態でSubmitボタンを押しますと

::> 830: Nothing imported from notations 

というエラー表示がnotation 部のPOLYEQ_3 の所に出ます。従ってconstructors の所へもPOLYEQ_3を加えてチェックをやり直してください。

 すると多分エラーは無いはずです。エラーがあれば本文中にコメントの形( :: をつけると行のそれ以後、改行までの文字列行がコメントになる )でエラー番号が入ります。その意味は本文中の最後の方に、やはりコメントの形で表示されます。またError Informationのところにもエラーが表示されます。もしエラーが無ければ何も表示されません。

 なお何度かチェックするとき、前のエラー番号が本文中に入ったまま、必要箇所を修正して、次のチェックをしてかまいません。システムは自動的に前のエラーコメントは消して、次のエラーコメントを(あれば)入れてくれます。

  チェック後の画面