現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編 Pureの型prop 命題論理の命題変数 論理式（一番標準的だと思える） 閉じた論理式（自由変数を含まない） 型がpropであるラムダ項 MLのデータ型thm MLのデータ型thmのデータインスタンス M…

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。 辞書的意味 証明が済んだ論理式（ほぼ、辞書的意味） ML言語のthmデータ…

全称束縛変数をパラメータと呼ぶらしい。Coqだと、公理をパラメータと呼んでいたりしたな。公理も作業仮説であり仮のものと考えると、文字通り仮引数だからだろう。理論を手続きと考えての仮引数。この発想だと、定理は出力＝戻り値か。理論を「証明の集まり…

TTYはダメだ、と言いながらOutputパネルはほぼTTY。そのため： 出力が長いときに、切られる。 出力から文字列を探せない。GUIでよくある「目でgrep」、辛い！ 出力がリンクやボタンであればいいのに。例外は thy_deps だが、ショボい。 コピペは出来る。が、…

attributeもテクニカルタームらしい。オプションとかアノテーションとかに近いものらしい。定理に対して、なんらかの付加情報を付ける働きがあるようだ。構文範疇にattributeがある。attributeは、'[' 名前 引数のカンマ区切り並び ']' の形で、ブラケットだ…

proof constantって、登録されてた定理のことかも。find_constsで定数を検索できる。その表示は、名前（ラベル）と型の組のリスト。find_theoremsでは、名前（ラベル）と命題（あるいはシーケント）の組のリスト。どちらも名前付けられているモノ。モノが項…

参照：よく分からん用語 - 檜山正幸のキマイラ飼育記 メモ編 solve -- テクニカルタームのこともある。goalをsolveする、というし、solved goalともいう。solve this problem とかは日常語だろう。 answer -- ユニフィケーションの結果である束縛をanswerと…

Isabelleの場合： 定理： 実装言語MLのデータ型thmとそのインスタンスを定理と呼び、それに引きずられている。実装レベルでは、たいていの概念がthmデータで表現されているので、なんでも定理（＝thm）となる。 ルール： オブジェクト論理（ユーザー定義の論…

論理屋が論理的な語りをしない／出来ない、という現実がある。諺に、「医者の不養生」「紺屋（こんや or こうや）の白袴」とかあるけど、ちょっと違うな。他人のために尽くしていて自分には手が回らない、ってのとは違う。「儒者の不身持（じゅしゃのふみも…