• 
  XML实用培训教...
  ￥21.33元
• 
  AutoCAD2...
  ￥45.82元
• 
  海底构造与地球物...
  ￥154.84元
• 
  逻辑公式的可满足...
  ￥14.22元
• 
  水价理论与实践
  ￥13.43元

逻辑公式的可满足性问题是计算机科学和人工智能中的著名问题．本书前三章主要介绍经典的命题逻辑和一阶谓词逻辑公式以及模态逻辑公式的可满足性判定算法，也介绍了有关的软件工具．第四章则介绍它们在离散数学研究、软件和硬件的形式验证与测试等方面的应用．
本书可供从事计算机科学和人工智能研究的有关人员阅读，也可供高等院校计算机专业的本科生和研究生参考．

• 暂时还没有任何用户评论

总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

全部咨询(共0条问答)

• 暂时还没有任何用户咨询内容

总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

用户名：	匿名用户
E-mail：
咨询内容：

• 序
  前言
  引言
  第一章命题逻辑
  §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其他
  结束语
  参考文献