数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| date | 内容(予定) | 資料 | 宿題 |
|---|
| 10/2 | 講義概要，Coq の動作確認 | 講義スライド(その0) | |
| 10/9 | 講義: Basics.v 前半 | 講義スライド(その1) |
nandb, and3, factorial, blt_nat, plus_id_exercise, mult_1_plus
(締切 10/24(水) 8:00) |
| 10/16 | 講義: Basics.v 後半 | 講義スライド(その2) |
zero_nbeq_plus_1, andb_true_elim2, basic_induction, plus_comm_informal, mult_comm (締切 10/30(火) 10:00)
|
| 10/23 | 演習 | | |
| 10/30 |
講義: Lists.v |
講義スライド(その3) |
snd_fst_is_swap, list_funs, alternate, bag_functions, list_exercises, beq_natlist (締切 11/7(水) 10:00) |
| 11/6 |
講義: Poly.v 前半 |
講義スライド(その4) |
split, hd_opt_poly, filter_even_gt7, partition, flat_map
(締切 11/14(水) 10:00) |
| 11/13 |
講義: Poly.v 後半 |
講義スライド(その5) |
override_example (ソースにコメントとして定理の意味を書くこと),
apply_exercise1, override_neq, sillyex1, sillyex2,
apply_exercise2, plus_n_n_injective
(締切 11/27(火) 10:00) |
| 11/20 |
演習 |
宿題コメントへの回答 | |
| 11/27 |
講義: Poly.v 後半の残り，Gen.v, 自然演繹 |
講義スライド(その6), ここまでのタクティック一覧, 自然演繹 |
override_shadow, override_same, apply_exercises,
gen_dep_practice, gen_dep_practice_opt
(締切 12/5(水) 12/14(金) 10:00) |
| 12/4 |
講義: 自然演繹，Prop.v |
講義スライド(その7) |
six_is_beautiful, nine_is_beautiful,
b_times2, b_timesm
(締切 12/12(水) 12/14(金) 10:00) |
| 12/11 |
講義: Prop.v |
講義スライド(その8) |
gorgeous_sum, beautiful__gorgeous, double_even,
ev__even, ev_sum, inversion_practice, ev_ev__ev
(締切 12/19(水) 10:00) |
| 12/18 |
講義: Prop.v, 単純型付ラムダ計算 |
単純型付ラムダ計算 |
ex_set, mytype, foo
(締切 12/26(水) 10:00) |
| 12/25 |
講義: 単純型付ラムダ計算(つづき)，Logic.v (前半) |
講義スライド(その9) |
proj2, and_assoc, even__ev, iff_properties,
or_distributes_over_and_2, bool_prop
(締切 1/9(水) 10:00) |
| 1/8 |
講義: Logic.v (後半)，自然演繹(まとめ)，期末試験について |
講義スライド(その10), 含意・全称量化以外の論理結合子・演習問題 |
contrapositive，not_both_true_and_false, not_eq_beq_false,
dist_not_exists, dist_exists_or, total_relation
(締切 1/23(水) 10:00)
|
| 1/22 |
講義室で演習 | | |
| 2/5 |
期末試験＠物理系校舎・物理系216 | | |