科目名 : 計算と論理

科目コード 90860
配当学年 3年
開講期 後期
曜時限 火曜・2時限
講義室 共通3(講義)・3号館情報処理演習室1(演習)
単位数 2
履修者制限
講義形態 講義
言語
担当教員 五十嵐(淳)

講義概要

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

評価方法

・期末試験 60%
・課題 40% (ほぼ毎回の課題をレポート形式で提出)
・随意課題を提出した場合,さらに加点する.

最終目標

1) 命題論理・述語論理の基礎を修得
2) プログラムに関する性質の厳密な証明を行う能力を修得
3) 型システムと数理論理学の間の深く関連する概念を習得

講義計画

項目 回数 内容説明
序論 1
関数型プログラミングとプログラムの検証 6 帰納的データ定義,型システム,多相性,高階関数,帰納法による証明
命題と証明 7 帰納的に定義される命題、自然演繹、論理結合子、量化子、等しさ
学習到達度の確認 1

教科書

・Benjamin C. Pierce 他著 "Software Foundations" (オンライン・テキストとして http://www.cis.upenn.edu/~bcpierce/sf/ から利用可能)

参考書

特になし

予備知識

アルゴリズムとデータ構造入門(91150)

授業URL

初回の講義中に伝える。

その他

当該年度の授業回数などに応じて一部省略,追加がありうる.