やっと分かった、refinement という言葉。定義はなかった。「悟れ」ということらしい。要するに、未完成の証明図を考えて、未完成部分に「・・・」のようなマーカーがあるとして、そのマーカー部分＝未完成の部分を埋める作業をrefinementと言っているらしい…

いつものことだが、証明支援系や論理の話が、だいたいイイカゲンで論理的でもフォーマルでもない記述が多くて困る。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]テクニカルタームと説明の地の文の区別がつかない。at show t…

writeln "\<alpha>" とかはアプリケーションレベルでのサポート。よって、#"a" はcharだが、#"\<alpha>" はcharにならない。Poly/MLのUnicodeサポート状況によるが、Unicode文字を文字および文字列に使えるはずだが、ASCII頭で凝り固まっている。</alpha></alpha>

Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 ウェンツェルの目標と志には全面的に賛同するが、なんか考えがとっちらかっている（一貫性がない、混乱している、中途半端）んじゃないの。 宣言的文書がほんとに…

タクティク、タクティカル（証明コンビネータ、推論コンビネータ）、ゴールなどは手続き的証明遂行の用語だよな。 ファクト、ゴール、サブゴールとかを宣言的証明の文脈で使われても意味わからん。 ファクトって何だよ？ ゴールって意味不明だろ→Coqの証明ゲ…

Isar = Intelligible semi-automated reasoning ってのは後付のコジツケだろう。MizarプロジェクトとIsabelleのIsaからだろう。Mizarは自然言語（英語）に近い、と言われている。ASCIIだけで数学記号を使ってないので、冗長でイヤンナル感じもする。let n be…

動詞：have, show, obtain, assume など 副詞：then, hence, finally, also, moreover, thus など 接続詞：and など その他： proof, qed, theorem, lemma など

letter ::= 名前開始文字 = ラテン文字|ギリシャ文字 名前文字 ::= 名前開始文字|数字|"_"|"'" ラテン文字とは普通の英字大文字小文字。まー、普通。ところが、名前内に下付き添字（subscript）が使える。添字は範囲ではなくて、1文字ずつ前置マークアップす…