面向人工智能的命题动态逻辑及其扩展研究

第1章 导论
1.1 本书的学术依据和提出背景
1.2 国内外研究状况及选题价值
1.3 动态逻辑：人工智能的基石
第2章 数学准备
2.1 记法约定
2.2 集合
2.3 关系
2.4 图和达格
2.5 格
2.6 超穷序数
2.7 集合算子
第3章 可计算性和复杂性
3.1 机器模型
3.2 不同种类的复杂性
3.3 可归约性和完全性
第4章 逻辑准备：等式逻辑与无穷逻辑
4.1 等式逻辑
4.2 无穷逻辑
第5章 程序推理
5.1 什么是程序？
5.2 状态和执行
5.3 程序结构
5.4 程序验证
5.5 外生逻辑和内生逻辑
第6章 正则命题动态逻辑
6.1 正则命题动态逻辑的句法
6.2 正则命题动态逻辑的语义
6.3 正则命题动态逻辑的计算序列
6.4 正则命题动态逻辑的可满足性和有效性
6.5 正则命题动态逻辑的演绎系统
6.6 正则命题动态逻辑的基本性质
6.7 编码霍尔逻辑
第7章 滤过和可判定性
7.1 Fischer-Ladner闭包
7.2 滤过和小模型定理
7.3 非标准模型上的滤过
第8章 正则命题动态逻辑的演绎完全性及其复杂性
8.1 演绎完全性
8.2 逻辑后承
8.3 复杂性
8.4 紧致性和逻辑后承
第9章 非正则命题动态逻辑
9.1 上下文无关程序
9.2 非正则命题动态逻辑的基本结论
9.3 不可判定的扩张
9.4 命题动态逻辑的可判定性扩张
9.5 关于单字母程序的进一步研究
第10章 命题动态逻辑的一些变种
10.1 确定性命题动态逻辑和while程序
10.2 受限测试
10.3 自动机表示
10.4 补运算和交运算
10.5 逆运算
10.6 良基和完全正确性
10.7 并发性和通信
第11章 带有程序量词的命题动态逻辑
11.1 引言
11.2 带有递归程序的命题动态逻辑
11.3 程序量化
11.4 超过分析层级的QPDL复杂性
11.5 猜想与未来的工作
第12章 命题动态逻辑中互模拟程序和逻辑等值程序
12.1 研究动机
12.2 命题动态逻辑的相关基础
12.3 过程演算
12.4 命题动态逻辑PDL
12.5 结论与未来的工作
附录
第13章 关于Patri网的命题动态逻辑扩展
13.1 引言
13.2 理论背景
13.3 研究背景
13.4 DS3逻辑
13.5 DS3逻辑可满足性的计算复杂性
13.6 DS3逻辑的应用实例
13.7 结论与未来的工作
第14章 命题动态逻辑的无缩并无切割规则的矢列演算
14.1 引言
14.2 命题动态逻辑的无切割的矢列演算——CSPDL演算
14.3 结构规则的可容许性
14.4 充足性定理
14.5 切割-消去定理
14.6 结论与未来的工作
第1 5章 命题动态逻辑的多类型显示演算
15.1 引言
15.2 相关知识准备
15.3 语言和规则
15.4 可靠性
15.5 完全性
15.6 切割-消去规则
15.7 关于保守性的开问题
15.8 结论与未来的工作
第16章 带有有穷多个变元的命题动态逻辑的复杂性和表达力
16.1 引言
16.2 句法和语义
16.3 带有有穷多个变元的命题动态逻辑的片段
16.4 结论与未来的工作
第17章 带有存储、恢复和并行合成算子的命题动态逻辑
17.1 引言和研究动机
17.2 句法和语义
17.3 实例解读
17.4 受限片段RSPDL的公理系统
17.5 受限片段RSPDL的完全性
17.6 结论与未来的工作
第18章 从交流更新逻辑到命题动态逻辑的程序转换器
18.1 引言
18.2 交流更新逻辑
18.3 经由Brzozowski等式的程序转换
18.4 程序转换的矩阵演算
18.5 新转换器的复杂性
18.6 结论与未来工作
参考文献
后记