| 序 前言 引言 第一章命题逻辑 §1.1命题逻辑简介 §1.2可满足性问题 §1.2.1合取范式的可满足性问题 §1.2.2约束满足问题 §1.3Davis??Putnam算法 §1.3.1DP算法 §1.3.2分支策略 §1.3.3其他提高效率的手段 §1.4局部搜索法 §1.5有序二叉判定图 §1.6语义表和Stalmarck方法 §1.6.1语义表 §1.6.2Stalmarck方法 §1.7其他途径 §1.7.1随机探索算法 §1.7.2转换为多项式问题 §1.7.3有向图 §1.7.4利用易解的特殊可满足性问题 §1.7.5约束逻辑程序设计 §1.8各种方法的分析、比较与结合 §1.8.1理论分析 §1.8.2通过实验结果来比较 §1.8.3回溯法与不完备方法的结合 第二章一阶谓词逻辑 §2.1一阶谓词逻辑简介 §2.2自动定理证明 §2.2.1前束范式和子句形式 §2.2.2Herbrand定理 §2.2.3基于消解原理的否证法 §2.2.4判定过程 §2.3模型的自动构造 §2.3.1用搜索法构造有限模型 §2.3.2转换成SAT §2.3.3SATCHMO和MGTP及其他方法 §2.4模型构造与定理证明 第三章模态逻辑 §3.1命题模态逻辑 §2.2命题模态逻辑公式的可满足性判定方法 §3.2.1语义表方法 §3.2.2翻译法 第四章应用 §4.1数学研究 §4.1.1组合学 §4.1.2抽象代数和逻辑 §4.2硬件测试与验证 §4.3软件开发中的形式化方法 §4.3.1逻辑和关系型规范的险证 §4.3.2状态转换式规范的一致性检查 §4.3.3程序验证与测试 §4.4人工智能及其他 §4.4.1机器人规划 §4.4.2资源调度 §4.4.3图像理解 §4.4.4其他 结束语 参考文献 |
内容加载中，请稍后...
商品评论（0条）