数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 |
|---|
| 1 | 10/6 | 導入, Basics.v | スライド0, スライド1 | テキスト Preface.v, Basics.v の予習，Coq 環境の構築，予習で生じた質問の報告(締切 10/13 10:30) |
| 2 | 10/13 | Basics.v | | 演習問題(締切 10/20 10:30: Basics.v の nandb, and_b3, factorial, blt_nat, plus_id_exercise), Induction.v の予習 |
| 3 | 10/20 | Induction.v | スライド2 | 演習問題(締切 10/27 10:30: Basics.v の andb_true_eliml2，Induction.v の basic_induction, double_plus, beq_nat_refl), 配布資料1の予習 |
| 4 | 10/27 | 単純型付ラムダ計算 | 配布資料1 | 配布資料1の予習，Lists.v (の最初の方)の予習 |
| (5) | 補講: 11/5(木５限)＠７号館情報２ | 単純型付ラムダ計算(つづき)，Lists.v | スライド3 | 演習問題(締切 11/17 10:30:
Lists.v の snd_fst_is_swap, list_funs)，Lists.v の残りの予習 |
| 5 | 11/10 | (休講) | | |
| 6 | 11/17 | Lists.v, Poly.v | スライド4 | 演習問題(締切 11/27(金) 10:30:
Lists.v の list_exercises, beq_natlist, hd_opt), Poly.v と配布資料2の予習 |
| 7 | 11/27(金２限) | Poly.v | | 演習問題(締切 12/8 10:30:
Poly.v の poly_exercises, split, flat_map, override_neq) と配布資料2の予習 |
| 8 | 12/1 | 教室での演習 | 問題集 | |
| 9 | 12/8 | System F, BasicTactics.v | 配布資料2 | |
| (10) | 補講 12/11(金５限) | BasicTactics.v | スライド5 | 演習問題(締切 12/22 10:30:
BasicTactics.v の
silly_ex, sillyex1, sillyex2, plus_n_n_injective,
beq_nat_true, destruct_eqn_practice) |
| 10 | 12/15 | (休講) | | |
| 11 | 12/22 | 自然演繹とCoq | 配布資料3 |
|
| 12 | 1/5 | Logic.v | スライド6 | 演習問題(締切 1/12 10:30:
Logic.v の
and_assoc, iff_properties, or_distributes_over_and_2,
contrapositive, not_both_true_and_false, false_beq_nat) |
| 13 | 1/12 | Prop.v, MoreLogic.v |
スライド7, スライド8
|
演習問題(締切 1/26 10:30:
Prop.v の
b_times2 (2), gorgeous_plus13 (1), gorgeous_sum (2),
ev_sum (2), inversion_practice (1),
MoreLogic.v の
dist_not_exists+ (1), dist_exists_or+ (2))
|
| 14 | 1/19 | カリーハワード同型対応 | 講義資料 | |
| 15 | 1/26 | 教室での演習，期末試験について | | |
| 期末試験 | 2/2 | | | |