計算論理： 課題2
PropLogc.v の問題をなるべく多く解いて、作成した PropLogic.vファイルを、
manaba を通じて、2015/11/4 (水) までに提出せよ。
PropLogic.v ファイルの問題の全てが解けていなくても、かまわないが、
不完全な証明をそのままにすると Coq でのチェックが、そこから下に行かな
いので、かならず、「不完全な証明はコメントにして、そこに Admitted. を
いれておく」こと。つまり、提出ファイルの一番下の行まで、Coqがエラーな
く通るようにしておくこと。
注: 一般に「レポートを提出してください」と私が言うときは、必ず説明をつけるように言う
が、この課題については、解答のみでよい。
50問もあるが、
全問を解かないといけないことはない。
良い成績を取りたい人は40問以上解くとよいが、
ex25 (25問目)まで解ければ、この課題としては OK である。
質問は、メールで complogic@logic.cs.tsukuba.ac.jp に送ること。