课程大纲

课程大纲

数理逻辑与程序理论

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

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

预修课程
离散数学

大纲内容
第一章 数理逻辑概述 3学时 眭跃飞
第1节 普通逻辑
第2节 数理逻辑
第3节 形式化方法
第二章 预备知识 3学时 眭跃飞
第1节 集合
第2节 关系,函数
第3节 数学归纳法
第三章 命题逻辑 3学时 眭跃飞
第1节 命题
第2节 命题逻辑的语言、语法
第3节 命题逻辑的语义
第四章 命题逻辑:形式推理 3学时 眭跃飞
第1节 推理的必要性
第2节 形式推演规则
第3节 形式证明
第五章 逻辑推论 3学时 眭跃飞
第1节 理解形式推演与逻辑推论的关系
第2节 命题逻辑中的布尔代数
第3节 永真公式的基本性质
第六章 命题逻辑:可靠性和完备性 3学时 眭跃飞
第1节 元语言
第2节 传递性和有限性
第3节 命题逻辑的可靠性和完备性(第一种证明方法)
第七章 命题逻辑:完备性定理 3学时 眭跃飞
第1节 协调公式集合
第2节 完备性的一般证明方法
第八章 命题逻辑:Gentzen系统 3学时 眭跃飞
第1节 公理系统
第2节 矢列式
第3节 Gentzen系统
第4节 Gentzen系统的可靠性和完备性
第九章 谓词逻辑 3学时 眭跃飞
第1节 谓词
第2节 代数结构
第3节 谓词逻辑的语言、语法
第4节 谓词逻辑的语义
第十章 谓词逻辑:形式推理 3学时 眭跃飞
第1节 替换
第2节 谓词逻辑的逻辑推论
第3节 谓词逻辑的形式推导规则
第4节 证明及其例子
第十一章 谓词逻辑:公理系统和Gentzen系统 3学时 眭跃飞
第1节 谓词逻辑的公理系统
第2节 矢列式
第3节 Gentzen系统
第4节 Gentzen系统的可靠性和完备性
第5节 算术公理系统和公理集合论
第十二章 模态逻辑 3学时 眭跃飞
第1节 逻辑应用中容易出现的问题
第2节 模态词
第3节 命题模态逻辑
第4节 模态逻辑应用中的问题
第十三章 答疑、作业题讨论 3学时 眭跃飞
第1节 答疑、作业题讨论
第十四章 数理逻辑闭卷考试 3学时 眭跃飞
第1节 数理逻辑闭卷考试
第十五章 程序理论概述 3学时 詹博华
第1节 程序理论简介
第2节 操作语义
第3节 实践部分:高阶逻辑简介
第十六章 霍尔逻辑(一) 3学时 詹博华
第1节 指称语义
第2节 霍尔逻辑第一部分
第3节 实践部分:Isabelle简介
第十七章 霍尔逻辑(二) 3学时 詹博华
第1节 霍尔逻辑第二部分
第2节 实践部分:函数式程序的验证
第十八章 霍尔逻辑(三) 3学时 詹博华
第1节 霍尔逻辑案例
第2节 实践部分:操作语义和指称语义
第十九章 分离逻辑(一) 3学时 詹博华
第1节 分离逻辑
第2节 实践部分:霍尔逻辑正确性证明
第二十章 分离逻辑(二) 3学时 詹博华
第1节 分离逻辑案例
第2节 实践部分:霍尔逻辑应用案例

教材信息
1、 《面向计算机科学的数理逻辑》,《形式语义导引》 陆钟万,周巢尘、詹乃军 2002,2017 科学出版社,科学出版社

参考书
1、 Mathematical Logic for Computer Science M.Ben-Ari 2012.0 Springer

课程教师信息
眭跃飞,1988年7月,中国科学院软件研究所,基础数学,博士;1988年7月-2001年4月,中国科学院软件研究所, 研究员.2001年5月至今,中国科学院计算技术研究所, 研究员,博士生导师(计算机软件与理论专业).研究方向是大规模知识处理的理论基础,知识表示.1996年以来在国内外主要数学和计算机科学刊物上发表论文70多篇. 主要研究成果:改进Guntsch和 Gediga关于 Wong 和Ziark猜测的结果;证明粗关系数据库中信息熵关于粗关系数据库的加细的单调性;提出分层在线调页算法.在可计算性理论方面, 独立或合作解决4个可计算性理论中的未解决问题;在可计算性理论研究中提出了同时及时允许的概念.
詹博华, 本科毕业于麻省理工学院,博士毕业于普林斯顿大学数学系。之后曾在麻省理工学院和慕尼黑工业大学任博士后。2018年8月加入中国科学院软件研究所,副研究员。研究方向为,定理证明和程序验证.研究成果发表于CAV, IJCAR, ITP和TACAS会议。对交互式定理证明器(Isabelle)和程序逻辑都有实际应用的经验。