型推論してくれるのはいいけど、その結果がどうであるかを知りたい。 autoで証明してくれるのはいいけど、何をしたのか教えてくれ。 resolutionで、ユニフィケーションの結果を教えてくれ。 何を考えてるかワカランぞ、教えてくれ。教えてくれないのか？ お…

proof method周辺 - 檜山正幸のキマイラ飼育記 メモ編 isar-refの"Chapter 7 Proof scripts"あたりに書いてある。 セオリーのトップレベルで使うキーワードはセオリーコマンド theoremなどのゴール提示コマンで証明モード（リーズニングモード）に入る。 証…

型の表記として、 [A, B] => B は許されている。 命題の表記として、[| P; Q |] ==> R は許されていない。まさかの未定義！ Pureを生で使ってはいけないのは、こういう変な癖があって使いにくいからか。この奇妙な文法の背景が分からない。

一番上はOK、NGとコメントしてあるのは構文エラー definition "right_unit_law == (!!n.(n + 0 == n))" definition "right_unit_law1 == !!n.(n + 0 == n)" (* NG *) definition "right_unit_law2 == (!!n. n + 0 == n )" definition "(right_unit_law3) == …

マダマダというか、ダメダメというか。とっても使いにくい。30年間作り続けてこのレベルってことは、あと30年くらいはかかるのかな、生きてネーよ、チクショー。次が欠けている。 情報検索機能 アウトライン機能 リソース管理機能 ビジュアライズ機能 情報の…

Title: Automated Theory Interpretation Author: Immanuel Normann Pages: 138 URL: https://svn.eecs.jacobs-university.de/svn/eecs/archive/phd-2008/normann.pdf 学位論文。歴史とか用語法とかまとめようと頑張っている。読み物としても面白い。この論…