コンテンツにスキップ

Mizar/環境部

出典: フリー教科書『ウィキブックス(Wikibooks)』
環境部では,引用する形式の書かれているファイル名を書きます。
::環境設定
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

ライブラリーファイル一覧