数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 |
|---|
| 1 | 10/4 | 導入, Basics.v |
スライド0, スライド1
|
テキスト Preface.v, Basics.v の予習，Coq 環境の構築，課題提出システム登録
|
| 2 | 10/11 | Basics.v, Induction.v |
スライド2
|
演習問題(締切 10/18 10:30: Basics.v の nandb, andb3, factorial, blt_nat, plus_id_exercise, andb_true_elim2)
|
| 3 | 10/18 | Induction.v(つづき), 単純型付ラムダ計算 |
配布資料1
|
演習問題(締切 11/1 10:30: Induction.v の basic_induction, double_plus, beq_nat_refl)
|
| 4 | 10/25 | 単純型付ラムダ計算(つづき)，Lists.v |
スライド3
|
|
| 5 | 11/1 | Lists.v (つづき), Poly.v |
スライド4
|
演習問題(締切 11/15 10:30:
Lists.v の snd_fst_is_swap, list_funs, list_exercises, beq_natlist, hd_error)
|
| 6 | 11/8 | Poly.v (つづき) |
|
演習問題(締切 11/29 10:30:
Poly.v の poly_exercises, split, flat_map, currying)
|
| 7 | 11/15 | 教室での演習 |
問題集
|
|
| 8 | 11/29 | System F, Tactics.v |
配布資料2,
スライド5
|
|
| 9 | 12/6 | Tactics.v, Logic.v |
スライド6
|
演習問題(締切 12/20 10:30:
Tactics.v の apply_exercises1, inversion_ex3, inversion_ex6, plus_n_n_injective,
beq_nat_true, destruct_eqn_practice)
|
| 10 | 12/13 | Logic.v |
|
演習問題(締切 1/10 10:30:
Logic.v の and_assoc, or_distributes_over_and_2or_distributes_over_and,
contrapositive, not_both_true_and_false, dist_exists_or, in_app_iff,
beq_nat_false_iff)
|
| 11 | 12/15 | 自然演繹と Coq |
配布資料3
|
|
| 12 | 12/20 | IndProp.v |
スライド7
|
演習問題(締切 1/24 10:30:
IndProp.v の ev_double, inversion_practice, ev_sum, le_exercises の一部
(le_trans と O_le_n と le_plus_l)
|
| 12/27 | (休講) |
|
|
| 13 | 1/17 | 教室での演習 |
|
|
| 14 | 1/24 | カリーハワード同型対応，ProofObjects.v |
講義資料, スライド8
| |
| 15 | 1/31 | 期末試験について |
|
|
| 期末試験 | 2/7 |
|
|
|