科目名 : 計算と論理

科目コード 90860
配当学年 (計)3年後期・(数)4年
開講期 後期
曜時限 火曜・2時限
講義室 情報1
単位数 2
履修者制限
講義形態 講義
言語
担当教員 佐藤雅彦

講義概要

数理論理学と型理論の基礎について講述する.論理体系と型理論体系は本質的に同じ構造を持つという観点に立ち,両者を一体のものとして,形式的体系と意味について述べる.また,講義を補完するため,論理体系と型理論体系を操作するソフトウェアを用いた演習を行う.

評価方法

最終目標

講義計画

項目 回数 内容説明
序論 2 命題と証明,型と項,形式と意味
命題論理と型理論 7 構文論と意味論,健全性・完全性,正規化,演習
算術と型理論 5 構文論と意味論,限量記号と依存型,帰納法,演習

教科書

特になし

参考書

特になし

予備知識

プログラミング入門(90010)

授業URL

資料・連絡事項等は,本講義のホームページ(http://www.sato.kuis.kyoto-u.ac.jp/~masahiko/cal/)に置く.

その他

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