【逻辑公式的可满足性判定-方法工具及应用】张健科学.pdf
博士丛书 逻辑公式的可满足性判定 方法、工具及应用 张健著
序 环顾当今世界,国家的发达,民族的振兴,无一例外地离不 开科学技术的推动作用,年轻博士们历来是科技队伍中最活跃、最富创造性的生力军,他们的科研成果是学科发展强有力的推动 力量,是体现一个国家高层次教育水平和科研水平的窗口．为了 系统地反映年轻博士们的科研成果,促使他们的快速成长,加强 国际国内的学术交流,在老一辈科学家的热心支持下,科学出版社决定出版一套《博士丛书》.我们指导思想是突出本丛书的学术性、创造性、新颖性、先 进性和代表性,使之成为所有青年博士平等竞争的学术舞台和优 秀科研成果的缩影.这套丛书以专著为主,并适时组织编写介绍学科最新进展的 综述性著作.
前言 数理逻辑是数学和计算机科学的基础:逻辑公式的可满足性 判定是计算机领域的一个重要问题:过去几十年,很多学者在这 方面做了大量的工作,取得了很大的进展。本书将重点介绍实际 可用的判定算法而不是可判定性、复杂性等理论结果.本书的主体分四章.前三章分别讨论经典的命题逻辑和一阶 谓词逻辑公式以及命题模态逻辑公式的可满足性判定算法,也提 到有关的软件工具.最后一章则介绍它们在离散数学研究、软件 和硬件的形式验证与测试等方面的应用,本书适合于从事计算机科学和人工智能研究的有关人员阅 读,也可供高等院校计算机软件和理论等专业的高年级本科生和 研究生参考.