| 専攻 | 選択・必修 | 開設時期 | 単位数 | 授業形態 | 担 当 | |||
| 情報電子 | 選択 | 2年後 | 2 | 講義 | 高山泰博 | |||
| 【授業の概要】 論理的な思考の基礎概念である第一階述語論理の定理証明技術を学び、この技術を取り込んだ論理プログラミングおよび演繹データベースとの関わりについて学ぶ。 | ||||||||
| 【学修の進め方】 座学形式で授業を進める。各自の担当箇所を割当て、受講ノートをまとめて提出する。演習課題をを課しながら理解度を深める。受講ノートと演習課題は次回の授業で提出する。 | ||||||||
| 【授業計画】 | 【授業項目】 | 【内 容】 | ||||||
| 1 回 | オリエンテーション | この授業で学ぶ内容について説明する。 | ||||||
| 2 回 | 命題論理（１） | 命題論理の定義、解釈、妥当性、矛盾性、充足可能性について学ぶ。 | ||||||
| 3 回 | 命題論理（２） | 命題論理の標準形、論理的帰結について学ぶ。 | ||||||
| 4 回 | 述語論理（１） | 述語論理の定義、解釈、妥当性、矛盾性、充足可能性について学ぶ。 | ||||||
| 5 回 | 述語論理（２） | 述語論理の冠頭標準形について学ぶ。 | ||||||
| 6 回 | 証明の手続き | 証明の手続きに関する考え方とSkolem標準形について学ぶ。 | ||||||
| 7 回 | エルブラン領域 | エルブラン領域と無限の解釈を有限の領域で扱う考える方法について学ぶ。 | ||||||
| 8 回 | 意味の木 | 証明を見つけることが意味の木を生成することであるという方法について学ぶ。 | ||||||
| 9 回 | エルブランの定理 | 述語論理で充足不能性を証明することと有限の閉じた意味の木を生成すること（具体例の有限集合で充足不能性を証明すること）が等価であることを学ぶ。 | ||||||
| 10 回 | 命題論理に対する導出原理 | エルブランの定理を機械的に実現する方法である導出原理について学ぶ。 | ||||||
| 11 回 | 述語論理に対する導出原理 | 第１階述語論理における導出原理について学ぶ。 | ||||||
| 12 回 | 導出原理の完全性 | 導出原理が完全であることにについて学ぶ。 | ||||||
| 13 回 | Horn節と論理プログラミング | 制限された述語論理式と論理型プログラミングについて学ぶ。 | ||||||
| 14 回 | 述語論理プログラミングと演繹データベース | 述語論理とプログラムおよびデータベースの関係について学ぶ。 | ||||||
| 15 回 | 試験 | 講義で学んだことについて理解度を問う。 | ||||||
| 16 回 | まとめ | 答案を返却し、解説する。 | ||||||
| 【到達目標】 | 述語論理による定理の自動証明に用いられる技術を習得する。さらに、論理と論理プログラミング、演繹データベースの基礎概念や関連性を説明できるようになる。 | 【徳山高専学習・教育目標】 | Ｃ１ | 【JABEE基準1(1)】 | d-2a | |||
| 【評価法】 | 試験結果×0.6＋課題（レポート）×0.2+受講ノート(レジュメ)×0.2で総合評価する。 | |||||||
| 【テキスト】 | 有川節夫・原口誠、「述語論理と論理プログラミング」（オーム社） 長尾真、淵一博、「論理と意味」（岩波書店） 横田一正・宮崎収兄、「新データベース論」（共立出版） | |||||||
| 【関連科目】 | 先修科目名：本科：データベース（４年）、知的情報処理（５年） | |||||||