Mizar/環境部
< Mizar
- 環境部では，引用する形式の書かれているファイル名を書きます。
::環境設定
environ
::--------------------------------------------------------------------------------------
::語彙、単語集（+,-,*,/,exp(),log(),...）
:: 対象・作用を表す用語を記しているファイル
vocabularies ARYTM, ARYTM_3, RELAT_1, ARYTM_1, ABSVALUE, SQUARE_1, XCMPLX_0, COMPLEX1, POLYEQ_3;
::--------------------------------------------------------------------------------------
::記号の作用範囲（整数+整数,実数+整数,...）
:: 対象・作用を表現するかを表しているファイル
notations 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;
::--------------------------------------------------------------------------------------
::同要素の集合体、群
registrations XREAL_0, REAL_1, NUMBERS, ARYTM_3, ZFMISC_1, XBOOLE_0, XCMPLX_0;
::--------------------------------------------------------------------------------------
::条件範囲(集)「整数:{0,1,2,3,...}」,「実数:-∞より上、∞未満」,「ブール:0,1」,...
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
::--------------------------------------------------------------------------------------
::定義(集)
definitions TARSKI, REAL_1, XREAL_0;
::--------------------------------------------------------------------------------------
::定理(集)ファイル
theorems AXIOMS, REAL_1, ABSVALUE, XREAL_0, XCMPLX_0, XCMPLX_1;
::--------------------------------------------------------------------------------------
::公理図式（A→B,￢A∨B,...）
schemes FRAENKEL, BINOP_1, SUBSET_1;
証明の型(まずはmodeで探してみる)
- schemes
- set ⊂ mode ⊂ cluster
- 要約ファイル(abstract file) : *.abs
- 証明ファイル(論文証明 file) : *.miz