isar-overviewのBNFによる構文範疇としては、fact ::= label 。labelの定義はないが、たぶん識別子だろう。論理式を識別する名前がラベルとすれば、factは論理式の名前ってことになる。 tutorialにはfactの定義はない。 isar-refには、logical contentとは、…

http://www4.di.uminho.pt/~mjf/pub/SFV-CurryHoward-2up.pdf にいいことが書いてある。 Shallow encoding (Logical Frameworks).The type theory is used as a logical framework, a meta system for encoding a specific logic one wants to work with. Th…

こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5） - 檜山正幸のキマイラ飼育記 : そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャ…

素直に「ルールXxxを適用する」と読まない！ ルールは常識的な上から下の推論図で描かれる。推論（リーズニング）は逆方向だから、 ルールXxxを逆適用する

Findタブって、find_* コマンドと同じじゃん。なんだよコレーー。

A proposition is a well-typed term of type prop, a theorem is a proven proposition. theoremはproven propositionsとか言っているが、 thmデータをtheoremと言っていることが一番多い感じ。 ポールソンは、theoremはruleだ、と言っているし、 ウェンツ…

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。 辞書的意味 Isar文書内で、theoremコマンドによるIsar文の後に続く部分 …

C-x 8 RET 221e RET C-x 8 RET infinity RET

基本は、滅茶苦茶、恣意的、行き当たりばったり、気分次第、その場限り、思い付きで、イイカゲン、ルール無し、である。が、たまに区別を要求するからタチが悪い！多用されて多義性が強い（オーバーロードが激しい）用語は、その意味を列挙した辞書を作るし…

「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…