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