週別授業計画

教材：

　林晋：数理論理学，コロナ社，1989.

概要：

　プログラムや人工知能のために用いられる論理式の正確な読み書きに慣れることに主眼を置く．また，述語論理の式の他に，ソフトウェア・ハードウェアの仕様記述や検証で用いられる時相論理の式なども学ぶ．

学習・教育目標：

　数学・コンピュータの要求仕様その他の事象の論理的取扱について学ぶと共に，一階述語論理の基礎について理解する．

授業計画：

第1週

(担当: 細野) 論理とは何か：実例・応用・様々な論理学

第2週

(担当: 細野) 命題論理：意味論，真理値表，真理関数，トートロジー

第3週

(担当: 細野) 1階述語論理の体系：自然演繹法(NK), 1階言語の定義，中間試験

第4週

(担当: 水谷) 情報処理で用いる数学や概念の記号化(, 1階述語論理の演習)

第5-6週

(担当: 水谷) 1階述語論理の演習

第7週

(担当: 水谷) 1階述語論理の演習，中間試験 

第8週

(担当: 細野) 1階理論：等号の公理，自然数論

第9週

(担当: 細野) 1階述語論理の意味論：数学構造，真理値評価，普遍妥当性，モデル，完全性

第10週

(担当: 水谷) プログラムの検証・解析に用いる様々な論理学について

参考書等：

　林晋：プログラム検証論，共立出版，1995.

予備知識・前提条件：

　特に無し．

オフィスアワー：

　金15:00-16:30 3E201または3E102

成績評価：

　期末試験(50%)，レポート及び演習成績(50%)により評価する．
3回を超える欠席を行った場合は上記の得点に(欠席回数-3)/10を乗じた点数を減点することにより得点を計算する．
つまり最終得点は(レポート・演習点+期末試験点)xmin{10, 13-欠席回数}/10である．
(例えば期末試験とレポート・演習で合計85点を得た者が5回欠席していたならば 85-85x(5-3)/10=68点が最終得点になる．3回しか欠席していないならば85点のままとする．)

教官メールアドレス：

　細野千春： hosono ＠ ailab.is.tsukuba.ac.jp
　水谷哲也： mizutani ＠ cs.tsukuba.ac.jp