数理論理学 - 合理的エージェントへの応用に向けて -
- 発行年月日
- 2014/10/30
- 判型
- A5
- ページ数
- 224ページ
- ISBN
- 978-4-339-02489-0
- 内容紹介
- 目次
数理論理学の諸概念に初めて接する大学2, 3年生を対象に，命題論理，述語論理，様相論理を，直感的にわかるさまざまな例題を通してできるだけ容易に解説。述語論理については，論理型言語Prologを解説する章を用意した。
1. 集合
1.1 集合の表し方
1.2 集合の要素や集合間の関係
2. 命題論理
2.1 命題論理の構文論
2.1.1 命題論理の論理式
2.1.2 演算子の優先順位を用いた論理式の省略形
2.2 命題論理の意味論
2.2.1 命題論理の意味領域
2.2.2 命題論理の解釈
2.2.3 命題論理の論理式の性質（恒真，充足可能，充足不能）
2.3 命題論理の論理式の等価性
2.4 タブローの方法
2.4.1 タブローの方法の概要
2.4.2 タブローの構成
2.4.3 構成規則の適用順序
2.4.4 タブローによる論理式の恒真性の証明方法
2.4.5 タブローの方法の健全性と完全性
2.5 命題論理の公理と推論規則
演習問題
3. 述語論理
3.1 述語論理の構文論
3.1.1 述語とは
3.1.2 述語論理で用いる記号とarity
3.2 述語論理の意味論
3.2.1 対象領域と割当て
3.2.2 述語論理の解釈
3.2.3 述語論理の論理式の性質（恒真，充足可能，充足不能）とモデル
3.3 述語論理の論理式の等価性
3.3.1 等価性の定義
3.3.2 限定子を含む等価な論理式
3.3.3 等価な論理式一覧（変換規則）
演習問題
4. 導出原理
4.1 論理式の標準形
4.1.1 冠頭標準形
4.1.2 冠頭連言標準形
4.1.3 スコーレム標準形
4.1.4 節集合
4.2 導出原理による推論
4.2.1 導出原理の概要
4.2.2 単一化とmgu
4.2.3 導出原理を用いた推論手順
4.3 導出原理の健全性と完全性
4.3.1 エルブラン解釈
4.3.2 エルブランの定理
演習問題
5. 様相論理
5.1 命題様相論理
5.1.1 様相演算子
5.1.2 命題様相論理の構文論
5.1.3 可能世界を用いた意味論
5.1.4 命題様相論理の論理式の性質
5.1.5 体系K
5.1.6 いろいろな様相論理
5.1.7 恒真な論理式と到達可能関係
5.2 命題線形時間時相論理
5.2.1 時相オペレータ
5.2.2 PLTLの構文論
5.2.3 PLTLの意味論
5.3 命題分岐時間時相論理CTL
5.3.1 経路限定子
5.3.2 CTL の構文論
5.3.3 CTL の意味論
5.4 命題分岐時間時相論理CTL*
5.4.1 CTL*の構文論.
5.4.2 CTL*の意味論
5.5 命題信念様相論理
5.5.1 信念オペレータ
5.5.2 命題信念様相論理の構文論
5.5.3 命題信念様相論理の意味論
5.5.4 命題信念様相論理の体系
演習問題
6. 合理的エージェント
6.1 意図の理論の概要
6.1.1 意図
6.1.2 計画
6.1.3 意図の理論の概要
6.2 BDI logic
6.2.1 心的状態の様相演算子
6.2.2 CTL*の拡張モデル
6.2.3 心的状態の様相と時相様相の二重構造の世界
6.2.4 イベントに関する論理式
6.2.5 BDI logic の構文論
6.2.6 BDI logic の意味論
6.3 合理的エージェントの振舞い
6.3.1 実践的推論
6.3.2 実践的推論の事例
6.3.3 実践的推論に関するBDI logic を用いた記述例
6.3.4 意図の実行
6.3.5 意図の実行に関するBDI logic を用いた記述例
6.4 コミットメント戦略の振舞い
6.4.1 コミットメント戦略
6.4.2 BDI logic を用いた記述例
6.4.3 意図の実行例
6.5 心的状態の整合性とモデルの制限
6.5.1 強い現実主義
6.5.2 虫歯治療の事例
6.5.3 心的状態の整合性の適用範囲
6.6 形式化のメリット
7. Prolog
7.1 Prolog の処理系SWI ? Prolog
7.1.1 SWI ? Prolog の入手方法
7.1.2 SWI ? Prolog のインストール方法
7.1.3 専用フォルダの準備とSWI ? Prolog の起動方法
7.2 簡単なプログラムによるProlog プログラミング
7.2.1 Prolog プログラム
7.2.2 プログラムの読込み
7.2.3 プログラムに誤りがある場合の対応
7.2.4 プログラムの表示（listing）
7.2.5 プログラムの利用方法1（ゴール節による問合せ）
7.2.6 プログラムの利用方法2（変数を含むゴール節）
7.3 一般的な確定節
7.3.1 規則の導入
7.3.2 コメント
7.3.3 複合的な条件の表現方法
7.3.4 ＼= と=
7.3.5 確定節，事実節，ゴール節，ホーン節
7.4 プログラムの手続的解釈とSLD 導出
7.4.1 手続き定義としての確定節と，手続き呼出しとしてのゴール節
7.4.2 SLD 導出
7.4.3 プログラムの実行順序
7.5 再帰処理
7.5.1 バックトラック
7.5.2 再帰処理を書く際の方針
7.6 リスト処理
7.6.1 リスト処理に用いられる項[ Head | Tail ]
7.6.2 リストに対する再帰処理
7.7 宣言的プログラミング
7.8 バックトラック制御用述語カット（cut）「! 」
7.9 算術演算を含むプログラムとカット
演習問題
引用・参考文献
索引
