情報検索法

Mizar ダメ出し

メタ情報 - 檜山正幸のキマイラ飼育記メモ編あたりから：http://fm.mizar.org/contents.html からMML IDで探す。例 Volume 1, 1990 http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf 例 Volume 2, 1991 http://fm.mizar.org/1991-2/pdf2-3/oppcat_1.pdf テ…

2016-12-14

サンプルを動くようにする：ほぼ解決

Mizar ハマリ所ダメ出し tips

::> 121: Disagreement of argument types ::> 191: Unknown schemeこれの原因は、environ部の不備だった。schemes NAT_1; だけではスキームのインポートが出来ない。 constructors NAT_1; が必須、これがないとUnknown schemeが出る。registrations NAT_1; …

2016-12-14

単数形

Mizar ハマリ所ダメ出し構文備忘

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？）しかし、 Make Environment, Mizar Ver. 8.1.04 (Win32/FPC) Copyright (c) 1990-2015 Associatio…

2016-12-14

ラベル名

Mizar ハマリ所ダメ出し

アイダースコアが入れられない！たぶん識別子構文は英数字だけなのだろう。

2016-12-14

vocファイル

Mizar ハマリ所ダメ出し

ホントによくハマる。まず、vocファイルを書く。空でもいいから書く。 vocabulariesディレクティブに自分の名前を書く！！！新しい名前を定義するときは必ずvocファイルにも書く。名前（トークン）を知らないと言われたらvocファイルを疑う。

2016-12-14

サンプルを動くようにする：努力段階

Mizar 具体例ダメ出し

environ :: From NAT_1 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1; notations T…

2016-12-14

サンプルを動くようにする：明らかな命題

Mizar tips

environがホントに難しいが、environ部を（もし）書けたら、明らかな命題を確認する。 INDUCT2: for n, m being Nat holds n + 1 = m + 1 implies n = m; INDUCT3: for n being Nat holds n + 0 = n; INDUCT4: for n, m being Nat holds n + (m + 1) = (n + …

2016-12-14

environのインポートディレクティブ

Mizar ダメ出し構文備忘

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？） constructors definitions theorems schemes requirements それ以外に次を確認している。 registr…

2016-12-14

envirn部のマージ

Mizar ダメ出し

NAT_1とO_RING_1のマージ例。そのまま2つをコピペしてもエラー。次のようにディレクティブごとに揃える。 environ :: From NAT_1, O_RING_1 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYT…

2016-12-14

environ部

Mizar ダメ出し

environ部のディレクティブは2度以上書けるようだが、同じアーティクルが2度以上指定されると、 *810: Directive name repeated これがシンドイ。コピペしかないのに、コピペに不便な仕様。

2016-12-14

中間ファイル

Mizar

.aco XML、ボキャブラリの計数情報のようだ。 .ano テキスト、謎だが、これもボキャブラリの計数情報のようだ。 .atr XML、謎 .cho テキスト、.anoと似てる。 .dct テキスト、タグジャンプファイルと似てる、なんかのインデックスっぽい。 .dcx XML、シンボ…

2016-12-14

バージョンが謎分かった

Mizar

配布ファイル： mizar-8.1.04_5.33.1254-i386-win32.exe ソフトウェアのバナー： Mizar Ver. 8.1.04 (Win32/FPC) doc/mml.txtの記述： Version 5.33.1254 配布ファイル名が、-〈システムバージョン〉_〈MMLバージョン〉- だった。