授業科目名				担当教官
記号論理特論				岩沼　宏治
時間割番号	単位数	コース	履修年次	期別	曜日	時限
414430 B	2	(未登録)	1	後期	木	VI
［概要と目標］
本講義では，記号論理の基礎と定理証明などの計算論的な諸概念と結果について講義する． 　デジタルコンピュータ上における計算の本質について理解することを目的としている．また講義の後半では，関連事項として大規模離散データの学習やデータマイニング技術の基礎と先進的な事項について講義する．
［必要知識・準備］
離散数学，ブール代数，アルゴリズムとデータ構造，情報理論,
［評価基準］
試験とレポートにより評価する．余裕があれば，プログラミング課題を出す．
［教科書］
(未登録)
［参考書］
(未登録)
［講義項目］
１．　記号論理とは？　構文と意味 　２．　充足可能性，恒真性，形式体系系と完全性および健全性 　３．　節論理，スコーレム関数とエルブランの定理 　４．　導出原理その１：　命題論理において 　５． ユニフィケーション 　６．　導出原理その２：　一階論理において 　７．　自動証明の高速化のための証明戦略：超導出法，支持集合法，線形導出法 　８．　自動証明の高速化のための技術：　包摂技術，補題法，　 　９．　節タブロー法とその高速化技術 １０．　ホーン節論理とPROLOG：　宣言的プログラミング １１．　離散データの学習：　決定木と情報利得 １２．　離散データのデータマイニング：　バケット解析 １３． 離散データのデータマイニング：　系列データ解析