数理逻辑与程序理论

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

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

离散数学

陆钟万，《面向计算机科学的数理逻辑》第二版,科学出版社,北京,2002. 周巢尘,詹乃军,《形式语义导引》,科学出版社,2017.

数理逻辑部分：
第一章 预备知识
集合，关系，函数，归纳定义和归纳证明。

第二章 命题逻辑
命题，命题逻辑的语言、语法和语义，逻辑推论，形式推演，范式，命题逻辑的可靠性和完备性。

第三章 一阶逻辑
量词，一阶逻辑的语言、语法和语义，逻辑推论，形式推演，前束范式。

第四章 可靠性和完备性
公式和公式集合的可满足性和有效性，公式集合的极大协调性，一阶逻辑的可靠性和完备性。

第七章 模态命题逻辑简介
模态命题语言，模态命题逻辑的语义、可靠性和完备性。

程序理论部分：
第一章计算逻辑， 包括Hoare逻辑，动态逻辑和时序逻辑。

第二章最弱前提条件和最强后条件演算。

M.Ben-Ari, Mathematical Logic for Computer Science, Springer，third edition, 2012. 李未,数理逻辑(第二版),2014. 眭跃飞,数理逻辑(草稿),2016.
David Gries, Science of Programming,Springer Verlag, New York, 1981, 350 pages.
E.W. Dijkstra, Principles of Programming, Prentice-Hall, 1976.

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