面向计算机科学的数理逻辑

本书对计算机科学方面的数理逻辑进行了综合介绍，涵盖命题逻辑、谓词逻辑、模态逻辑与代理、二叉判定图、模型检测和程序验证等内容。

迈克尔·休斯（Michael Huth）现任纽伦堡科技大学（UTN）创始校长。在加入UTN之前，休斯教授曾在伦敦帝国理工学院工作，历任计算机科学教授、计算机系主任，并将继续担任客座教授。在研究和教学方面，他目前的研究重点是人工智能和网络安全领域的前瞻性课题。<br /><br />马克·莱恩（Mark Ryan）伯明翰大学计算机科学学院计算机安全教授，也是伯明翰大学安全与隐私中心的负责人。他的主要研究方向包括机器学习的安全性、应用密码学和安全协议、安全系统分析、隐私计算等。

译者序<br />第1版序<br />第2版前言<br />致谢<br /><br />第1章　命题逻辑1<br />　1.1　判断语句1<br />　1.2　自然演绎3<br />　　1.2.1　自然演绎规则4<br />　　1.2.2　派生规则15<br />　　1.2.3　自然演绎总结17<br />　　1.2.4　逻辑等价19<br />　　1.2.5　侧记：反证法19<br />　1.3　作为形式语言的命题逻辑20<br />　1.4　命题逻辑的语义23<br />　　1.4.1　逻辑连接词的含义23<br />　　1.4.2　数学归纳法25<br />　　1.4.3　命题逻辑的合理性28<br />　　1.4.4　命题逻辑的完备性30<br />　1.5　范式33<br />　　1.5.1　语义等价、满足性和<br />有效性34<br />　　1.5.2　合取范式和有效性36<br />　　1.5.3　霍恩子句和可满足性41<br />　1.6　SAT求解机42<br />　　1.6.1　线性求解机43<br />　　1.6.2　三次求解机45<br />　1.7　习题50<br />　1.8　文献注释61<br />第2章　谓词逻辑62<br />　2.1　我们需要更丰富的语言62<br />　2.2　作为形式语言的谓词逻辑65<br />　　2.2.1　项66<br />　　2.2.2　公式66<br />　　2.2.3　自由变量和约束变量68<br />　　2.2.4　代换69<br />　2.3　谓词逻辑的证明论71<br />　　2.3.1　自然演绎规则71<br />　　2.3.2　量词的等价77<br />　2.4　谓词逻辑的语义80<br />　　2.4.1　模型81<br />　　2.4.2　语义推导85<br />　　2.4.3　相等的语义86<br />　2.5　谓词逻辑的不可判定性86<br />　2.6　谓词逻辑的表达能力89<br />　　2.6.1　存在式二阶逻辑91<br />　　2.6.2　全称式二阶逻辑91<br />　2.7　软件的微观模型92<br />　　2.7.1　状态机93<br />　　2.7.2　Alma重观95<br />　　2.7.3　软件的微模型97<br />　2.8　习题102<br />　2.9　文献注释113<br />第3章　通过模型检测进行验证115<br />　3.1　验证的动机115<br />　3.2　线性时态逻辑117<br />　　3.2.1　LTL的语法117<br />　　3.2.2　LTL的语义118<br />　　3.2.3　规范的实际模式122<br />　　3.2.4　LTL公式之间的重要等价123<br />　　3.2.5　LTL的适当连接词集124<br />　3.3　模型检测: 系统、工具和性质124<br />　　3.3.1　例: 互斥124<br />　　3.3.2　NuSMV模型检测器127<br />　　3.3.3　运行NuSMV129<br />　　3.3.4　重温互斥129<br />　　3.3.5　摆渡者难题132<br />　　3.3.6　交错位协议134<br />　3.4　分支时间逻辑138<br />　　3.4.1　CTL的语法138<br />　　3.4.2　计算树逻辑的语义139<br />　　3.4.3　规范的实际模式142<br />　　3.4.4　CTL公式间的重要等价142<br />　　3.4.5　CTL连接词的适当集143<br />　3.5　CTL^*与LTL和CTL的<br />表达能力144<br />　　3.5.1　CTL中时态公式的布尔<br />组合145<br />　　3.5.2　LTL中的过去算子146<br />　3.6　模型检测算法146<br />　　3.6.1　CTL模型检测算法146<br />　　3.6.2　具有公平性的CTL模型<br />检测151<br />　　3.6.3　LTL模型检测算法153<br />　3.7　CTL的不动点特征157<br />　　3.7.1　单调函数158<br />　　3.7.2　SAT_EG的正确性159<br />　　3.7.3　SAT_EU的正确性160<br />　3.8　习题161<br />　3.9　文献注释168<br />第4章　程序验证170<br />　4.1　为什么要规范和验证编码170<br />　4.2　软件验证的一种框架171<br />　　4.2.1　一种核心程序设计语言172<br />　　4.2.2　霍尔三元组173<br />　　4.2.3　部分正确性和完全<br />正确性175<br />　　4.2.4　程序变量和逻辑变量176<br />　4.3　部分正确性的证明演算177<br />　　4.3.1　证明规则177<br />　　4.3.2　证明布景180<br />　　4.3.3　案例研究：最小和截段189<br />　4.4　完全正确性的证明演算192<br />　4.5　合同编程194<br />　4.6　习题196<br />　4.7　文献注释200<br />第5章　模态逻辑与代理202<br />　5.1　真值的模式202<br />　5.2　基本模态逻辑202<br />　　5.2.1　语法202<br />　　5.2.2　语义204<br />　5.3　逻辑工程208<br />　　5.3.1　有效公式储备209<br />　　5.3.2　可达关系的重要性质210<br />　　5.3.3　对应理论212<br />　　5.3.4　一些模态逻辑214<br />　5.4　自然演绎216<br />　5.5　多代理系统中的知识推理218<br />　　5.5.1　一些例子218<br />　　5.5.2　模态逻辑KT45^n220<br />　　5.5.3　KT45^n的自然演绎223<br />　　5.5.4　例子的形式化224<br />　5.6　习题230<br />　5.7　文献注释236<br />第6章　二叉判定图237<br />　6.1　布尔函数的表示237<br />　　6.1.1　命题公式和真值表237<br />　　6.1.2　二叉判定图239<br />　　6.1.3　有序BDD242<br />　6.2　简约OBDD的算法246<br />　　6.2.1　算法reduce246<br />　　6.2.2　算法apply247<br />　　6.2.3　算法restrict249<br />　　6.2.4　算法exists249<br />　　6.2.5　OBDD的评价251<br />　6.3　符号模型检测252<br />　　6.3.1　表示状态集合的子集253<br />　　6.3.2　表示迁移关系255<br />　　6.3.3　实现函数pre_?和pre_?255<br />　　6.3.4　综合OBDD 256<br />　6.4　关系μ演算257<br />　　6.4.1　语法和语义258<br />　　6.4.2　对CTL模型及规范说明的<br />编码260<br />　6.5　习题263<br />　6.6　文献注释274<br />参考文献275