CSS と Coq の記事が並ぶというシュールな展開ですが、これも嫌だ力のなせるわざです。今日の証明では SearchPattern とか eapply がでてくるよ！ 本日のお題は、 filter 関数を2回適用しても結果のリストの長さが変わらないという性質 FilterLength の証明…

Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明す…

今日は久しぶりの勉強会でした。まずは id:suer さんによる、 PPL Summer School のレポートでした。SAT Solver が超速い！みたいな。問題の制約を SAT の形式(?)にエンコードできれば、すごい速さで問題を解くことができるそうです。すげーな。 次は id:yos…

読んでた。結構おもしろい。けど、"Paradoxes of classical predicate calculus" と題されたとこが謎。英語力が足りないのか論理学の知識が足りないのか。 あと、forall とか exists とかの扱いがいまいちわかってない気がするな。坂部先生の資料で自然演繹…