工学部情報学科

計算と論理 (科目コード 90860)

日時 火曜日2限(10:30〜12:00)
場所 総合研究7号館情報1講義室
担当教員:五十嵐 淳 (igarashi)
オフィスアワー:火曜日 15:00〜17:00 (総合研究7号館224)
(その他の時間は要アポイントメント)
担当TA:

お知らせ

自習の進め方(宿題について)

  1. 教科書の該当する章のファイルを Proof General (もしくは CoqIDE) で読み込む.
  2. Coq への読み込みコマンドを使いながら教科書を読み進める.
  3. 練習問題の指示に従ってファイルを書き換える(解答を埋める).
  4. Coq に読み込ませてみて,背景が青(緑)になれば無事に Coq のチェックに通った,ということ.
  5. 宿題提出システム(パスワード発行はこちら)を使って該当ファイルを zip したものをアップロードする.

Proof General, CoqIDE の操作

機能 Proof General CoqIDE (メニュー操作)
一歩読み進める(Coq にテキストの内容を送信) C-c C-n Navigation → Forward
一歩戻る (undo) C-c C-u Navigation → Backward
カーソル位置まで進む(戻る) C-c RET Navigation → Go to
ファイル末尾まで読み込む C-c C-b Navigation → End
証明すべき命題(ゴール)を表示 C-c C-p
既になされた証明・定義を表示 C-c C-t
SearchAbout C-c C-a C-a Queries → SearchAbout (F2)

講義内容(シラバスより)

数理論理学の基礎と,数理論理学を用いた計算機プログラムの検証について講述する.また,講義を補完するため,証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う.

講義スケジュールと配布資料

回数date内容(予定)資料宿題
110/1導入・オンライン教科書のインストールスライドBasics.v の予習
210/8Basics.v (Coq による関数型プログラミング)スライド演習問題(締切 10/22 10:30: nandb, andb3, factorial, blt_nat),Induction.v の予習
310/22Basics.v, Induction.v (帰納法による証明)スライド 演習問題(締切 10/29 10:30: Basics.v の plus_id_exercise, mult_S_1, zero_nbeq_plus_1, Induction.v の basic_induction, double_plus, beq_nat_refl),次週の予習
410/29 単純型付ラムダ計算 資料 次週の予習
511/5 単純型付ラムダ計算(型付け), Lists.v スライド 演習問題(締切 11/12 10:30: Lists.v の fst_swap_is_snd, list_funs, list_exercises, beq_natlist),次週の予習
611/12 Lists.v の残り, Poly.v スライド 演習問題(締切 11/19 10:30: Lists.v の hd_opt, Poly.v の split, poly_exercises, partition, flat_map),次週の予習
711/19 System F, MoreCoq.v 前半 資料, スライド
811/26 MoreCoq.v 後半 演習問題(締切 12/3 10:30: MoreCoq.v の silly_ex, sillyex1, sillyex2, plus_n_n_injective, beq_nat_true, gen_dep_practice, override_shadow, destruct_eqn_practice)
912/3 自然演繹と Coq 資料 次週の予習
1012/10 命題論理とカリー・ハワード同型対応 資料
1112/17 Logic.v スライド 演習問題(締切 1/7 10:30: Logic.v の and_assoc, iff_properties, or_distributes_over_and_2, contrapositive, not_both_true_and_false, false_beq_nat)
121/7 Prop.v スライド 演習問題(締切 1/14 10:30: Prop.v の double_even, ev_sum, b_times2, gorgeous_plus13, gorgeous_sum, inversion_practice)
131/14 MoreLogic.v (前半) スライド 演習問題 (締切 1/21 10:30: MoreLogic.v の dist_not_exist, dist_exists_or)
141/21 演習 問題集
151/28 演習
期末試験2/4

リソース

教科書
Benjamin C. Pierce 他著 Software Foundations (ダウンロード用: sf-201309.zip)
参考書
教科書の和訳版(内容の食い違いについては教科書の記述を優先します.)
Coq: INRIA の公式サイト
ProofGeneral
emacs から Coq を操作するためのソフトウェア

igarashi@kuis.kyoto-u.ac.jp
Last update on $Date:: 2012-01-29 23:40:47 +0900#$