数理逻辑与程序理论

课程编码：085400M05015T 英文名称：Mathematical Logic and Theory of Programming 课时：38 学分：2.00 课程属性：专业普及课 主讲教师：李勇坚等

本课程为计算机科学与技术学科研究生的学科基础课。数理逻辑与程序理论是计算机科学的基础。计算机科学各个分支均有相应的逻辑，比如信息安全的BAN逻辑，程序设计理论的Hoare逻辑，人工智能中的各种逻辑等等。描述逻辑现在应用在计算机各分支中。本课程将陈述这些逻辑中最基本的内容，即命题逻辑、一阶逻辑和模态逻辑。其中命题逻辑、一阶逻辑和计算逻辑将全面介绍，包括逻辑的背景、语言、语法、语义、形式推演以及可靠性和完备性定理。模态逻辑只介绍基本概念及其应用。
通过本课程的学习，要求学生能掌握数理逻辑与程序理论的基本概念、理论和方法，对命题逻辑、一阶逻辑和计算逻辑的整体内容有所了解，为进一步学习和研究计算机科学与技术打下一个理论基础。

无

第一章 预备知识 2学时
第1节 集合，关系，函数，归纳定义和归纳证明。
第二章 命题逻辑 4学时
第1节 命题，命题逻辑的语言、语法和语义，逻辑推论，形式推演，范式，命题逻辑的可靠性和完备性。
第三章 一阶逻辑 6学时
第1节 量词，一阶逻辑的语言、语法和语义，逻辑推论，形式推演，前束范式。
第四章 可靠性和完备性 6学时
第1节 公式和公式集合的可满足性和有效性，公式集合的极大协调性，一阶逻辑的可靠性和完备性。
第五章 定理证明 6学时
第1节 SAT和SMT及交互式定理证明和各种求解工具、定理证明器。
第六章 模态和时序逻辑 4学时
第1节 模态命题逻辑的语义、可靠性和完备性。
第七章 计算逻辑 6学时
第1节 包括Hoare逻辑，动态逻辑和时序逻辑。
第八章 最弱前提条件和最强后条件 4学时
第1节 最弱前提条件和最强后条件演算

詹乃军，中国科学院软件研究所研究员，研究领域为实时和混成系统、信息物理融合系统、形式化方法、计算语义模型、程序验证。
李勇坚，中国科学院软件研究所副研究员，研究领域为形式化方法、形式验证、机器学习、网络安全。