工学部情報学科

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

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

お知らせ

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

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

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

回数date内容(予定)資料宿題
110/3 導入, Basics.v スライド0, スライド1 テキスト Preface.v, Basics.v の予習,Coq 環境の構築,課題提出システム登録
210/10
310/17
410/24
510/31
611/7
711/14
811/21
911/28休講(?)
1012/5
1112/12
1212/19
1312/26
141/9
151/30
期末試験

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

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

FAQ

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)

リソース

教科書
本講義用 lf-201710.zip (MD5SUM: 11e145790d5e5b367ef0b56e3dafd67e): Benjamin C. Pierce 他著 Software Foundations シリーズ 第1巻 Logical Foundations (本家は時おりバージョンアップがあるので使わないでください.)
参考書
ボランティアによる教科書の和訳版(元になった版は2011年版です.内容の食い違いについては教科書の記述を優先します.)
Coq: INRIA の公式サイト
ProofGeneral
emacs から Coq を操作するためのソフトウェア. Version 4.4.1~pre 以降を使ってください. Ubuntu は zesty (16.10) 以降にはパッケージがあります. macOS の Homebrew にも proof-general パッケージがあります.
Company-Coq
ProofGeneral の拡張集. forall と打つと ∀ で表示されたりするのでうれしい. 自動補完などもできる.

五十嵐 淳