数理逻辑与程序理论

课程编码：180086081202P2001H 英文名称：Mathematical Logic and Theory of Programming 课时：60 学分：3.00 课程属性：专业核心课 主讲教师：眭跃飞

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

离散数学

第一章 导论 詹博华
第1节 逻辑-推理 1.0学时
第2节 逻辑-概念 1.0学时
第3节 逻辑-悖论 1.0学时
第二章 基础知识 詹博华
第1节 集合 1.0学时
第2节 函数 1.0学时
第3节 对角线方法 2.0学时
第4节 自然数 2.0学时
第三章 命题逻辑 詹博华
第1节 被形式化对象 1.0学时
第2节 形式语言 1.0学时
第3节 形式语法 1.0学时
第4节 形式语义 1.0学时
第四章 命题逻辑2 詹博华
第1节 形式推导 1.0学时
第2节 例子 1.0学时
第3节 可靠性定理 1.0学时
第五章 命题逻辑3 詹博华
第1节 完备性定理 2.0学时
第2节 形式证明的例子 1.0学时
第3节 范式定理 1.0学时
第4节 SAT问题 1.0学时
第六章 一阶逻辑 詹博华
第1节 代数结构 1.0学时
第2节 形式语音 1.0学时
第3节 形式语法 1.0学时
第4节 形式语义 1.0学时
第七章 一阶逻辑2 詹博华
第1节 形式证明的例子 2.0学时
第2节 可靠性定理 1.0学时
第3节 完备性定理 2.0学时
第4节 Gentzen系统 1.0学时
第5节 Gentzen系统的完备性定理 2.0学时
第八章 可计算性 詹博华
第1节 图灵机 1.0学时
第2节 可计算函数 1.0学时
第3节 递归定理 0.5学时
第4节 图灵度简介 0.5学时
第九章 Goedel不完全性定理 詹博华
第1节 自然数结构 1.0学时
第2节 可计算函数的可定义性和可表示性定理 1.0学时
第3节 不完全性定理的简要证明 1.0学时
第十章 模态逻辑 詹博华
第1节 人工智能中的模态词 1.0学时
第2节 命题模态逻辑 1.0学时
第3节 一阶模态逻辑简介 1.0学时
第十一章 Hoare逻辑 詹博华
第1节 Hoare逻辑 1.0学时
第2节 语义 0.5学时
第3节 相对完备性 1.0学时
第4节 Hoare完备性为什么困难 0.5学时
第十二章 时序逻辑 詹博华
第1节 时序逻辑 1.0学时
第2节 完备性定理 1.0学时
第3节 时态逻辑 1.0学时
第十三章 人工智能中的时间逻辑 詹博华
第1节 时间的表示 1.0学时
第2节 本体 1.0学时
第3节 时间在本体中的位置 1.0学时
第十四章 知识表示中的问题 詹博华
第1节 命题逻辑 0.5学时
第2节 谓词逻辑 1.0学时
第3节 模态逻辑 1.5学时

眭跃飞,1988年7月，中国科学院软件研究所，基础数学，博士;1988年7月-2001年4月，中国科学院软件研究所, 研究员.2001年5月至今,中国科学院计算技术研究所, 研究员,博士生导师(计算机软件与理论专业).研究方向是大规模知识处理的理论基础，知识表示.1996年以来在国内外主要数学和计算机科学刊物上发表论文70多篇. 主要研究成果：改进Guntsch和 Gediga关于 Wong 和Ziark猜测的结果；证明粗关系数据库中信息熵关于粗关系数据库的加细的单调性；提出分层在线调页算法.在可计算性理论方面, 独立或合作解决4个可计算性理论中的未解决问题；在可计算性理论研究中提出了同时及时允许的概念. 交互式定理证明器（Isabelle）和程序逻辑都有实际应用的经验。