题名:
判定过程   / (英) 丹尼尔·克勒宁, (以) 奥弗·施特里希曼著 , 蔡少伟译
ISBN:
978-7-115-66220-0 价格： CNY159.80
语种:
chi
载体形态:
352页 图 24cm
出版发行:
出版地： 北京 出版社： 人民邮电出版社 出版日期： 2025
内容提要:
本书系统介绍了各种可判定的一阶理论及其在自动软件和硬件验证、定理证明与编译器优化等场景中的具体应用, 涵盖了可满足性（SAT）求解器和可满足性模理论（SMT）求解器的核心技术, 以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题, 并借助高效的判定过程进行求解。 
主题词:
计算机算法  
中图分类法:
TP301.6 版次： 5
其它题名:
SAT与SMT求解算法
主要责任者:
克勒宁 著
主要责任者:
施特里希曼 著
次要责任者:
蔡少伟 译
责任者附注:
丹尼尔·克勒宁(Daniel Kroening), 牛津大学计算机科学系的教授, 他的兴趣包括自动验证、软件工程和编程语言。 
责任者附注:
奥弗·施特里希曼(Ofer Strichman), 以色列理工学院工业工程与管理学院的教授, 他的研究兴趣包括软件和硬件的形式化验证, 以及一阶逻辑片段的决策程序。 
责任者附注:
蔡少伟, 中国科学院软件研究所研究员, 国内约束求解领域领军人物。多次夺得国际SAT与SMT比赛冠军, 在CAV、CP、SAT等顶级会议获得最佳论文与杰出论文奖, 担任相关国际顶级会议程序委员会主席。