| 开本：16开 |
| 纸张：胶版纸 |
| 包装：平装-胶订 |
| 是否套装：否 |
| 国际标准书号ISBN：9787115662200 |
| 所属分类：图书>计算机/网络>程序设计>CC++C#VCVC++ |
新华书店正版，关注店铺成为会员可享店铺专属优惠，团购客户请咨询在线客服！编辑推荐
·填补空白：作为约束求解领域稀缺教材，适配学术研究与工程实践双重需求 ·主创团队：牛津 以色列理工学院两位领域先驱合著，蔡少伟研究员倾力翻译，译文严谨贴合原著精髓 ·案例实操：通过大量工业级案例演示复杂问题向逻辑模型的转化过程，助力理论落地应用 ·内容多维：系统覆盖可判定一阶理论、 求解核心算法与建模语言，兼顾理论深度与工程细节 ·名家力荐位国际国内院士、学会主席等联名推荐，认可其参考价值
内容简介
本书系统介绍了各种可判定的一阶理论及其在自动软件和硬件验证、定理证明与编译器优化等场景中的具体应用，涵盖了可满足性（）求解器和可满足性模理论（）求解器的核心技术，以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题，并借助高效的判定过程进行求解。本书不仅为研究人员提供了丰富的理论知识，还为高级软件工程师和开发者提供了实用的参考指南。
本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读。
作者简介
丹尼尔·克勒宁（ ），高级首席科学家，生成式初创公司 的联合创始人，曾任牛津大学计算机科学系教授，研究兴趣包括自动验证、软件工程和编程语言。
奥弗·施特里希曼（ ），以色列理工学院数据与决策科学系教授，现任该校计算方向副主任，主要研究形式化验证、求解器、程序等价性验证等，曾获年奖。
蔡少伟，中国科学院软件研究所研究员，国内约束求解领域领军人物。多次夺得国际 与比赛军，在 、、等很好会议获得很好论文与杰出论文奖，担任相关国际很好会议程序委员会主席。其研发的求解器应用于芯片验证、操作系统验证及工业调度。
目 录
第章 简介和基本概念
形式推理的两种方法
基于推演的证明
基于枚举的证明
推演与枚举
基本定义
范式及其属性
理论视角
我们求解的问题
如何介绍理论
表达能力与可判定性
逻辑公式的布尔结构
逻辑作为建模语言
习题第章 简介和基本概念
形式推理的两种方法
基于推演的证明
基于枚举的证明
推演与枚举
基本定义
范式及其属性
理论视角
我们求解的问题
如何介绍理论
表达能力与可判定性
逻辑公式的布尔结构
逻辑作为建模语言
习题
符号表
第章 命题逻辑的判定过程
命题逻辑
求解器
……
显示全部信息
媒体评论
逻辑推理的判定过程，是自动推理技术革命的核心。这场革命已在工业领域展现出广泛应用，从硬件与软件验证，到云服务正确性的保障，乃至更多关键领域。有人认为，这些技术将在解决生成式机器学习模型的“幻觉”问题上发挥关键作用。本书是该领域最有价值的入门读物。两位作者作为自动推理领域的先驱和知名专家，不仅对最重要的方法提供了算法细节，还深入探讨了其背后的逻辑与计算基础，最后介绍了这些技术的应用场景。对于任何想了解这一前沿方向的读者而言，本书都是不可或缺的读物。如今，其中文版得以问世，我深感欣喜。 —— ，德国弗赖堡大学计算机体系结构讲席教授、国际学会前任主席 这本经典著作是最早也是至今专享的系统阐述可满足性模理论（）核心概念的教材。更重要的是，其内容至今仍对想要了解该领域的读者具有极高的参考价值。书中几乎涵盖了现代求解相关的所有重要主题，尤其侧重算法解析与实例演示，这一特点使得不同背景的读者都能轻松理解书中内容。 —— ，斯坦福大学计算机系教授、著名自动推理专家、会士 在过去的年里，已成为自动推理领域的领先技术。由该领域两位前沿研究人员丹尼尔·克勒宁和奥弗·施特里希曼所著的《判定过程：与求解算法（第版）》是这一重要领域的权威教科书。我很高兴看到蔡少伟研究员将此书翻译成中文，让中国的本科生和研究生能够接触到这部重要著作。 —— ，美国莱斯大学计算工程系杰出教授、著名形式化方法专家、美国国家科学院美国国家工程院美国艺术与科学院院士 在我的大脑中，经常会出现两个声音：一个推崇科学之美，另一个推崇很好工程。在我的认知中，可判定的一阶理论以及与求解器，正是计算机领域中一座连接科学与工程的桥梁。蔡少伟研究员是约束求解方向的很好学者，其倾力翻译的《判定过程：与求解算法（第版）》这本经典著作，系统地介绍了这个方向的基础理论、重要算法、核心技术以及具体应用，必将会促进该方向在国内的发展，意义深远。值得一提的是，书中每一章最后专门讲述了相关知识的演进脉络与幕后故事，其中蕴藏着科学技术发展的内在规律，极富启发性。 ——包云岗，中国科学院计算技术研究所副所长、中国科学院大学计算机学院副院长 本书系统介绍了可判定一阶理论及其应用，是该领域的优秀教材。我国约束求解专家蔡少伟研究员将该书倾力翻译为中文，具有深远意义。强烈推荐所有形式化方法领域的研究者、技术开发者以及相关工程应用人员学习和参考。 ——王戟，国防科技大学研究员、形式化方法专业委员会前任主任 本书由国际知名学者丹尼尔·克勒宁与奥弗·施特里希曼合著，是计算机科学领域的一本经典教材。该书从算法视角系统地介绍了一阶理论的可判定性问题，聚焦与求解器的核心技术，通过大量实际场景甚至工业级的案例展现了算法和求解器在应用中的威力。无论是对于计算机专业学生、算法工程师，还是对形式化验证感兴趣的研究人员来说，该书都是一本关于与求解的涵盖理论、算法和工程落地的重要参考书。蔡少伟研究员以深厚的学术功底和对与求解的深刻洞见，把握原著精髓，译文严谨流畅，为国内读者提供了一个快捷进入该领域前沿的途径。 ——夏壁灿，北京大学数学科学学院教授 是计算机科学和人工智能领域的重要基础问题之一。自世纪末以来，求解算法取得了巨大进步。是其扩展，能接受更加丰富的约束形式。和求解算法及工具推动了软件分析、测试和验证的发展。本书是较早介绍和求解技术的专著，在国际上有重要影响，虽然不是尽善尽美，但有助于读者深入了解该领域。我相信，该书中文版的出版，将吸引更多的国内学者加入这一领域，或使用该领域的成果。 ——张健，中国科学院软件研究所研究员、会士
显示全部信息
商品详情
·填补空白：作为约束求解领域稀缺教材，适配学术研究与工程实践双重需求 ·主创团队：牛津 以色列理工学院两位领域先驱合著，蔡少伟研究员倾力翻译，译文严谨贴合原著精髓 ·案例实操：通过大量工业级案例演示复杂问题向逻辑模型的转化过程，助力理论落地应用 ·内容多维：系统覆盖可判定一阶理论、 求解核心算法与建模语言，兼顾理论深度与工程细节 ·名家力荐位国际国内院士、学会主席等联名推荐，认可其参考价值
内容简介
本书系统介绍了各种可判定的一阶理论及其在自动软件和硬件验证、定理证明与编译器优化等场景中的具体应用，涵盖了可满足性（）求解器和可满足性模理论（）求解器的核心技术，以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题，并借助高效的判定过程进行求解。本书不仅为研究人员提供了丰富的理论知识，还为高级软件工程师和开发者提供了实用的参考指南。
本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读。
作者简介
丹尼尔·克勒宁（ ），高级首席科学家，生成式初创公司 的联合创始人，曾任牛津大学计算机科学系教授，研究兴趣包括自动验证、软件工程和编程语言。
奥弗·施特里希曼（ ），以色列理工学院数据与决策科学系教授，现任该校计算方向副主任，主要研究形式化验证、求解器、程序等价性验证等，曾获年奖。
蔡少伟，中国科学院软件研究所研究员，国内约束求解领域领军人物。多次夺得国际 与比赛军，在 、、等很好会议获得很好论文与杰出论文奖，担任相关国际很好会议程序委员会主席。其研发的求解器应用于芯片验证、操作系统验证及工业调度。
目 录
第章 简介和基本概念
形式推理的两种方法
基于推演的证明
基于枚举的证明
推演与枚举
基本定义
范式及其属性
理论视角
我们求解的问题
如何介绍理论
表达能力与可判定性
逻辑公式的布尔结构
逻辑作为建模语言
习题第章 简介和基本概念
形式推理的两种方法
基于推演的证明
基于枚举的证明
推演与枚举
基本定义
范式及其属性
理论视角
我们求解的问题
如何介绍理论
表达能力与可判定性
逻辑公式的布尔结构
逻辑作为建模语言
习题
符号表
第章 命题逻辑的判定过程
命题逻辑
求解器
……
显示全部信息
媒体评论
逻辑推理的判定过程，是自动推理技术革命的核心。这场革命已在工业领域展现出广泛应用，从硬件与软件验证，到云服务正确性的保障，乃至更多关键领域。有人认为，这些技术将在解决生成式机器学习模型的“幻觉”问题上发挥关键作用。本书是该领域最有价值的入门读物。两位作者作为自动推理领域的先驱和知名专家，不仅对最重要的方法提供了算法细节，还深入探讨了其背后的逻辑与计算基础，最后介绍了这些技术的应用场景。对于任何想了解这一前沿方向的读者而言，本书都是不可或缺的读物。如今，其中文版得以问世，我深感欣喜。 —— ，德国弗赖堡大学计算机体系结构讲席教授、国际学会前任主席 这本经典著作是最早也是至今专享的系统阐述可满足性模理论（）核心概念的教材。更重要的是，其内容至今仍对想要了解该领域的读者具有极高的参考价值。书中几乎涵盖了现代求解相关的所有重要主题，尤其侧重算法解析与实例演示，这一特点使得不同背景的读者都能轻松理解书中内容。 —— ，斯坦福大学计算机系教授、著名自动推理专家、会士 在过去的年里，已成为自动推理领域的领先技术。由该领域两位前沿研究人员丹尼尔·克勒宁和奥弗·施特里希曼所著的《判定过程：与求解算法（第版）》是这一重要领域的权威教科书。我很高兴看到蔡少伟研究员将此书翻译成中文，让中国的本科生和研究生能够接触到这部重要著作。 —— ，美国莱斯大学计算工程系杰出教授、著名形式化方法专家、美国国家科学院美国国家工程院美国艺术与科学院院士 在我的大脑中，经常会出现两个声音：一个推崇科学之美，另一个推崇很好工程。在我的认知中，可判定的一阶理论以及与求解器，正是计算机领域中一座连接科学与工程的桥梁。蔡少伟研究员是约束求解方向的很好学者，其倾力翻译的《判定过程：与求解算法（第版）》这本经典著作，系统地介绍了这个方向的基础理论、重要算法、核心技术以及具体应用，必将会促进该方向在国内的发展，意义深远。值得一提的是，书中每一章最后专门讲述了相关知识的演进脉络与幕后故事，其中蕴藏着科学技术发展的内在规律，极富启发性。 ——包云岗，中国科学院计算技术研究所副所长、中国科学院大学计算机学院副院长 本书系统介绍了可判定一阶理论及其应用，是该领域的优秀教材。我国约束求解专家蔡少伟研究员将该书倾力翻译为中文，具有深远意义。强烈推荐所有形式化方法领域的研究者、技术开发者以及相关工程应用人员学习和参考。 ——王戟，国防科技大学研究员、形式化方法专业委员会前任主任 本书由国际知名学者丹尼尔·克勒宁与奥弗·施特里希曼合著，是计算机科学领域的一本经典教材。该书从算法视角系统地介绍了一阶理论的可判定性问题，聚焦与求解器的核心技术，通过大量实际场景甚至工业级的案例展现了算法和求解器在应用中的威力。无论是对于计算机专业学生、算法工程师，还是对形式化验证感兴趣的研究人员来说，该书都是一本关于与求解的涵盖理论、算法和工程落地的重要参考书。蔡少伟研究员以深厚的学术功底和对与求解的深刻洞见，把握原著精髓，译文严谨流畅，为国内读者提供了一个快捷进入该领域前沿的途径。 ——夏壁灿，北京大学数学科学学院教授 是计算机科学和人工智能领域的重要基础问题之一。自世纪末以来，求解算法取得了巨大进步。是其扩展，能接受更加丰富的约束形式。和求解算法及工具推动了软件分析、测试和验证的发展。本书是较早介绍和求解技术的专著，在国际上有重要影响，虽然不是尽善尽美，但有助于读者深入了解该领域。我相信，该书中文版的出版，将吸引更多的国内学者加入这一领域，或使用该领域的成果。 ——张健，中国科学院软件研究所研究员、会士
显示全部信息
商品详情