2010年10月08日のツイート
@kururu_goedel: $A\subseteq A\cup B$と$(A\cup B)\cap C\subseteq(A\cap C)\cup B$の証明をCoqで書いた。
@kururu_goedel: 今セメはいろいろあって、火曜と木曜の夕食は運転しながらマクドナルドがデフォルト
@kururu_goedel: えーと、先週は二回、昼食と夕食が運転しながらでした。
@kururu_goedel: いや、妻からすれば私はこのレベルで人間関係の機微を理解していないんだろうなと思うので、なんとか理解してもらいたいと思うのだけれども、良いやり方が思いつかない。
@kururu_goedel: 「集合が等しいのは入っている元が同じってことだよね」「はい」「一つめには$\{\emptyset\}$が入ってないよね」「はい」「二つめには$\{\emptyset\}$が入っているよね」「はい」「だからこの二つは等しくないよね」「なんで?」の繰り返しで。
@kururu_goedel: 昨日は、$\{\emptyset\}$と$\{\emptyset, \{\emptyset\}\}$が等しくないというのがわからないという学生さんとしばらく押し問答してしまった。
@kururu_goedel: シャーマニックプリンセスのエンディングの歌の中にあるモノローグを正確に言えなくなってしまったのが少し悲しい
@kururu_goedel: っていうか、うちの大学のCS学科に形式手法のこと研究している人がいるみたいだったのでメール書いたけど、一日たってまだ返事が来ない
@kururu_goedel: もちろん、ある程度の数学的センスのある人にとってはproverでやるのは苦痛だけれども、「定義を使って分解する」とか「論理的に議論をすすめる」とかに慣れていない人達にとっては、即時に応答が返ってくるinteractive proverはむしろよい練習かもしれない。
@kururu_goedel: 学生さんたちの証明になっていない証明を読んで、どこが間違っているのかを説明するのに疲れてきたので、もういっそのことCoqかなんかで証明させる練習したほうが早いかもしれないとか思い始めているところ。
@kururu_goedel: OpenOfficeのデフォルト登録名がMicrosoftになっていたのはどういうことか