Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。 Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。 Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。 Isarの前…

Natural Deduction Mizar SerND → introduction assume assume + use → elimination – apply ∧ introduction thus concat ∧ elimination – select ∨ introduction – add ∨ elimination per cases cases ∀ introduction let for ∀ elimination – instantiate …

名前の管理が甘い、名前空間が粗末 ユニコードを考慮してない。アスキー偏重。 Mizar以外は、スクリプト言語またはそのシンタックスシュガー。 ブロック構造を意識してないか曖昧。 文書構造を意識してないか粗末 型クラスがあと付けで歪んでいたり問題を抱…

Mizar Isar let fix assume assume set let set def consider ... such that obtain ... where take (no equivalent) per cases ... proof ... qed suppose next assume (no keyword) have thus show hence then show thesis (?thesis) proof ... end proof …

型クラス相当機能は分かったが、 型クラスのインスタンス化の方法が分からない。 インスタンス化に証明が伴うが、書き方が分からない。is を使って、X is C と書いて、この命題を証明するのか？

パターンがあるものは、3分間・URIテンプレート - 檜山正幸のキマイラ飼育記 で示す。 http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/ http://mizar.org/version/current/html/{小文字ID}.html http://mizar.org/JFM/pdf/{小文字ID}.pdf http://fm.miza…

http://mizar.org/version/current/html/ hidden tarski_0 tarski xboole_0 xboole_1 enumset1 xfamily xregular xtuple_0 zfmisc_1 subset_1 setfam_1 relat_1 fanct_1 ordinal1 ordinal2 ordinal3 relat_2 wellord1 wellord2 funct_2 funct_3 funct_4 grun…

適当な訳語がない。等力かな。集合が等力とは、1:1対応があること、基数が等しいこと。

$MIZFILE/mml.larにすべてのアーティクルの名前（list of articlesだろう）。mml.vctにすべてのシンボル。

environは地獄だ。environはノービスには書けない。エキスパートが書いてあげるのが前提みたいだ。スライド http://mizar.org/cicm_tutorial/mizar.pdf "Mizar Hands-on Tutorial" by Adam Naumowicz, Artur Korni lowicz, Adam Grabowski (July 29, 2016) …

メタ情報 - 檜山正幸のキマイラ飼育記 メモ編 あたりから：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 テ…

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

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…

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

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

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…

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 + …

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

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…

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

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

配布ファイル： 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バージョン〉- だった。

記述書式（format） 述語や関数を呼び出すときの記述形式、定義時に指定する。 座（ローカス、ローサイ）（locus, loci） 述語や関数のパラメータ宣言 パターン 記述書式と関係あるようだが現在は不明 Mizarでは公理と定理の区別がなく、すべて定理： 公理定…

i, j, k, l, m, n は 自然 数 とする。 このとき i + k = j + k ならば i = j 証明: まず 述語を定義する: P[自然 数] とは i + $1 = j + $1 ならば i=j であること。 (A1): P[0] ※帰納法のベース 証明: 次を仮定する: (B0): i + 0 = j + 0 。 このとき (B1)…

http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…

名前がないからどうにもならないが、名無し／メタ情報なしでも、 特定シンボル（述語名、関数名、モード名、属性名）を含む定理 特定のプロファイルの特定のシンボルを含む定理 特定のアーティクルで定義された特定のシンボルを含む定理 存在命題、全称命題…

http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、 :: The drinker's principle reserve x for object; ex x st P x implies for y holds P y proof per cases; suppose A0: ex x st not P x; consider a such that A1: not P a by …

the system Declare by D. Syme ？？ 不明 the Mizar mode for HOL by J.Harrison http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html the Isar language for Isabelle by M. Wenzel http://isabelle.in.tum.de/Isar/ Mizar-light for HOLlight by F. Wiedij…

地獄の作業例。 reserve i,j,k,l,m,n for natural number; i+k = j+k implies i=j; proof defpred P[natural number] means i+$1 = j+$1 implies i=j; A1: P[0] proof assume B0: i+0 = j+0; B1: i+0 = i by INDUCT:3; B2: j+0 = j by INDUCT:3; hence thesi…

論理 Mizar ⊥ contradiction ¬φ not φ φ ∧ ψ φ & ψ φ ∨ ψ φ or ψ φ ⇒ ψ φ implies ψ φ ⇔ ψ φ iff ψ ∃ x. ψ ex x st ψ ∀ x. ψ for x holds ψ ∀ x.(φ ⇒ ψ) for x st φ holds ψ nonは形容詞の否定、andとsuch thatはスクリプト言語のキーワード。