这是一本结合逻辑在计算机科学中的应用来介绍数理逻辑的教科书。书中主要介绍了消解定理证明、逻辑式程序设计和非经典逻辑(模态逻辑和直觉主义逻辑)，所用的方法与数理逻辑的经典著作有很大不同，更加适合研究计算机理论的读者，可以帮助他们更好地理解计算机理论中的许多概念，是一本真正面向计算机科学的逻辑著作。另外，每章最后给出了进一步阅读建议，书末又分主题给出了相当多的参考文献，便于读者深入学习。

本书不要求读者具备逻辑基础知识，适合计算机科学系和数学系高年级本科生以及低年级研究生使用。

本书是介绍数理逻辑的基础教材，不仅覆盖了传统的基本内容(语法、语义、可靠性、完全性和紧致性)，而且很大一部分是讨论非传统的内容，诸如消解定理证明、逻辑式程序设计和非经典逻辑(模态逻辑和直觉主义逻辑)，而这些主题在现代计算机科学中变得越来越重要。

本书讲述的内容广泛，深入浅出，简明易懂，适合作为计算机科学系和数学系高年级本科生以及低年级研究生的教材。

出版者的话

专家指导委员会

译者序

中文版序

前言

绪论

第一章 命题逻辑

第一节 序和树

第二节 命题、联结词和真值表

第三节 真值指派和赋值

第四节 命题演算中的表证明

第五节 表证明的可靠性和完全性

第六节 前件演绎和紧致性

第七节 公理方法

第八节 消解

第九节 加细消解

第十节 线性消解、Horn子句和PROLOG

进一步阅读建议

第二章 谓词逻辑

第一节 谓词和量词

第二节 语言：项和公式

第三节 形成树、结构和列表

第四节 语义：含义与真值

第五节 PROI；OG程序解释

第六节 证明：完全系统表

第七节 表证明的可靠性和完全性

第八节 公理化方法

第九节 前束范式和斯科朗化

第十节 厄布朗定理

第十一节 合一

第十二节 合一算法

第十三节 消解

第十四节 加细消解：线性消解

进一步阅读建议

第三章 PROLOG

第一节 SLD一消解

第二节 执行：搜索与回溯

第三节 执行的控制：cut

第四节 PROLOG程序终止的条件

第五节 相等

第六节 因失败而否定

第七节 否定和非单调逻辑

第八节 可计算性与不可判定性

进一步阅读建议

第四章 模态逻辑

第一节 可能性与必然性；知识或信念

第二节 框架和力迫

第三节 模态表

第四节 可靠性和完全性

第五节 模态公理和特殊的可达关系

第六节 公理化方法

进一步阅读建议

第五章 直觉主义逻辑

第一节 直觉主义与构造主义

第二节 框架和力迫

第三节 直觉主义表

第四节 可靠性和完全性

第五节 可判定性和不可判定性

第六节 比较指南

进一步阅读建议

第六章 集合论基础

第一节 集合论中的一些基本公理

第二节 集合的布尔代数

第三节 关系、函数和幂集公理

第四节 自然数、算术和无穷

第五节 替换、选择和基础

第六节 谓词逻辑中的策梅洛一弗兰克尔集

合论

第七节 基数：有穷和可数

第八节 序数

第九节 序数算术和超穷归纳

第十节 超穷递归、选择和有秩全域

第十一节 基数和基数算术

进一步阅读建议

附录A 历史回顾

附录B 一个家谱数据库

参考文献