授業科目名 : 計算と論理

科目コード 90860
配当学年 (計)3年 (数)4年
開講年度・開講期 平成30年度・後期
曜時限 火曜・2時限
講義室 総合研究7号館情報1
単位数 2
履修者制限
授業形態 講義
使用言語 日本語
担当教員    所属・職名・氏名 情報学研究科・教授・五十嵐淳

授業の概要・目的

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

成績評価の方法・観点及び達成度

・期末試験 70%
・課題 30% (7回程度の課題をレポート形式で提出)
・随意課題を提出した場合,さらに加点する.

到達目標

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

授業計画と内容

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

教科書

・Benjamin C. Pierce 他著 "Software Foundations" (オンライン・テキストとして http://www.cis.upenn.edu/~bcpierce/sf/ から利用可能、ただし講義で使用する版は別に配布する)

参考書等

特になし

履修要件

アルゴリズムとデータ構造入門(91150)、プログラミング言語(90170)を履修していること。

授業外学習(予習・復習)等

講義2回に1回程度宿題を課す。

授業URL

http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/

その他(オフィスアワー等)

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