The Coq Proof Assistant A Tutorial

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