高级数理逻辑-付宇课程教学大纲.docVIP

PAGE9

《高级数理逻辑》教学大纲

课程英文名称

AdvancedSymbolicLogic

开课院系

计算机科学与技术学院

课程类别

学位课（学科基础课）

授课对象

1.学术型2.专业学位

授课方式

1.讲授类

课程总学时

36

课程总学分

2

开课学期

1

适用专业

计算机科学与技术、计算机技术

预修课程

离散数学

主讲教师1

付宇

职称

副教授

主讲教师2

王静

职称

讲师

课程简介（500字以内）：

本课程适合于计算机科学与技术专业的研究生进行的专业基础课学习，内容涉及了计算机科学所依赖的数理逻辑学科中的高级部分，是与计算机科学有紧密联系并且相互之间又共同促进的数理逻辑应用性内容，包括经典逻辑和非经典逻辑中的构造性逻辑和模态逻辑，包括自然演绎系统、逻辑系统的合理性与完备性、合取范式与有效性、可满足性与求解机、作为形式语言的谓词逻辑、谓词逻辑的证明论和语义、线性时态逻辑、模型检测器、分支时态逻辑、模型检测算法等，反映了计算机科学中数理逻辑的新发展和实际需要。

课程教学目标与基本要求：

作为一级学科学位课，本课程开设目标在于使低年级研究生能够掌握对于计算机科学而言最为基础和重要的经典与非经典逻辑，能够了解其在软件工程形式化方法、模型检测与验证、高效算法及实现等方面的现代应用。课程要求学生掌握谓词逻辑、模态逻辑、模型检测、程序验证等。

课程考核方式和成绩计算评定：

1．考核方式：考试（√）；考查（）

2．成绩评定：

总评成绩构成：平时考核（40）％；中期考核（0）％；期末考核（60）％

平时成绩构成：考勤考纪（40）％；作业（60）％；读书报告（0）％

实践环节（0）％；其他（0）％

课程内容及详细教学计划：

授课内容（细化到章、节、目）

教学目标

授课模式（指传统讲授、讨论、多媒体教学等）

第一章、形式系统概论

1.1形式系统的定义

掌握形式系统的基本概念

传统讲授

1.2形式系统的元语言和元理论

掌握元语言和元理论的基本概念

传统讲授

1.3元理论关于语义和语构的研究

掌握语义和语构的相互关系

传统讲授

第二章、命题逻辑

2.1自然演绎系统

掌握自然演绎规则及其派生，逻辑等价的概念，反证法的运用。

传统讲授

2.2作为形式语言的命题逻辑

掌握命题逻辑的形式化构成。

传统讲授

2.4范式

掌握语义等价性、可满足性和有效性的概念；掌握合取范式的有效性和霍恩子句的可满足性。

传统讲授

2.5SAT求解机

掌握一般合适公式的可满足性求解机制。

传统讲授

第三章、谓词逻辑

3.1作为形式语言的谓词逻辑

掌握谓词逻辑的项、公式、自由变量、约束变量、代换等基本概念。

传统讲授

3.2谓词逻辑的证明论

掌握谓词逻辑的自然演绎规则

传统讲授

3.3谓词逻辑的语义

传统讲授

3.4谓词逻辑的表达能力及不可判定性

传统讲授

第四章、模型检测

4.1线性时态逻辑

掌握LTL语法、语义

传统讲授

4.2NuSMV模型检测器

掌握模型检测的系统、工具和性质

传统讲授

4.3分支时间逻辑

掌握CTL的语法和语义

传统讲授

4.4模型检测算法

掌握CTL和LTL模型检测的算法

传统讲授

4.5CTL的不动点

掌握CTL的不动点特征和可满足性验证算法的正确性。

传统讲授

教材及教学参考资料

教材

序号

教材名称

编著者

出版单位

出版时间

1

面向计算机科学的数理逻辑：系统建模与推理（第二版）

（德）哈斯，（英）瑞安

机械工业出版社

2007年

参考资料

序号

参考资料名称

编著者

出版单位

出版时间

1

数理逻辑教程(英文)

JohnBell

世界图书出版公司

2015年

注：1.课程类别参考培养方案，学位课明细到公共必修课、学科基础课和学科必修课；

2.主讲教师1和授课教师2两栏必填。