引言 1
第一章 命题逻辑 3
1.1 命题逻辑简介 3
1.2 可满足性问题 9
1.2.1 合取范式的可满足性问题 9
1.2.2 约束满足问题 11
1.3 Davis-Putnam算法 16
1.3.1 DP算法 17
1.3.2 分支策略 20
1.3.3 其他提高效率的手段 23
1.4 局部搜索法 28
1.5 有序二叉判定图 33
1.6.1 语义表 41
1.6 语义表和St？lmarck方法 41
1.6.2 St？lmarck方法 45
1.7 其他途径 48
1.7.1 随机探索算法 48
1.7.2 转换为多项式问题 50
1.7.3 有向图 52
1.7.4 利用易解的特殊可满足性问题 54
1.7.5 约束逻辑程序设计 56
1.8 各种方法的分析、比较与结合 57
1.8.1 理论分析 57
1.8.2 通过实验结果来比较 58
1.8.3 回溯法与不完备方法的结合 61
第二章 一阶谓词逻辑 63
2.1 一阶谓词逻辑简介 63
2.2 自动定理证明 70
2.2.1 前束范式和子句形式 71
2.2.2 Herbrand定理 76
2.2.3 基于消解原理的否证法 78
2.2.4 判定过程 84
2.3 模型的自动构造 86
2.3.1 用搜索法构造有限模型 86
2.3.2 转换成SAT 100
2.3.3 SATCHMO和MGTP及其他方法 104
2.4 模型构造与定理证明 107
第三章 模态逻辑 110
3.1 命题模态逻辑 110
3.2 命题模态逻辑公式的可满足性判定方法 114
3.2.1 语义表方法 114
3.2.2 翻译法 117
4.1.1 组合学 125
4.1 数学研究 125
第四章 应用 125
4.1.2 抽象代数和逻辑 128
4.2 硬件测试与验证 133
4.3 软件开发中的形式化方法 139
4.3.1 逻辑和关系型规范的验证 139
4.3.2 状态转换式规范的一致性检查 143
4.3.3 程序验证与测试 145
4.4 人工智能及其他 146
4.4.1 机器人规划 146
4.4.2 资源调度 148
4.4.3 图像理解 150
4.4.4 其他 151
结束语 153
参考文献 157