致远数理逻辑课程大纲

1、数理逻辑课程大纲 、课程简介 课程名称：数理逻辑 学时 /学分： 52/3 先修课程：离散数学 面向对象： ACM 班 教学目标： 在学生已掌握了集合论知识的基础上， 进一步介绍数理逻辑在计算机科学中 的应用， 加强计算机专业本科生的逻辑思维能力培养。 本课程除了介绍经典 的命题逻辑和谓词逻辑， 还介绍对计算机科学的发展很有影响力的模态逻辑 和直觉逻辑。 主要内容： 本课程先介绍命题逻辑和谓词逻辑中的重要思想方法和结论，然后引出逻辑 编程，介绍模态逻辑和直觉逻辑，最后介绍时序逻辑和模型检测。 、教学内容 第一章 命题逻辑 消解原理。 主要内容：命题演算， Tableau 证明方法，可靠性和完备

2、性的证明， 重点与难点：如何证明可靠性和完备性。 第二章 谓词逻辑 主要内容：谓词逻辑的语法、语义，可靠性和完备性证明，Herbrand 定理， Unification 。 重点与难点：如何证明可靠性和完备性。 第三章 PROLOG 主要内容： SLD 消解， 基于搜索和回溯的实现，可计算性和不可判定性。 重点与难点： SLD 消解和实现方法。 第四章 模态逻辑 主要内容：模态 Tableaux，可靠性和完备性。 重点与难点：如何证明可靠性和完备性。 第五章 直觉逻辑 主要内容：直觉 Tableaux, 可靠性和完备性，可判定性和不可判定性。 重点与难点：如何证明可靠性和完备性。 第六章 其它

3、逻辑 主要内容：计算机科学中用到的其它逻辑如时序逻辑、线性逻辑等；模型检测思想。 重点与难点：时序逻辑和模型检测。 三、教学进度安排 教学内容 教学形式 作业 第一周 命题逻辑，Tableau方法，可靠性和完备性 课堂教学 第二周 公理化方法 课堂教学 第三周 消解，线性消解，Horn字句 课堂教学 第四周 谓词逻辑，Tableau方法，可靠性和完备性 课堂教学 第五周 公理化方法，Herbrand定理，Unification 课堂教学 第六周 消解，线性消解 课堂教学 第七周 SLD消解，实现方法：搜索与回溯 课堂教学 第八周 Prolog程序终止条件，等式 课堂教学 第九周 可计算性与不可

4、判定性 课堂教学 第十周 知识与信念逻辑 课堂教学 第十 卜一周 模态Tableau方法，可靠性，完备性 课堂教学 第十二周 模态公理，公理化方法 课堂教学 第十三周 直觉主义与构造主义，Tableau方法，可靠完备性 课堂教学 第十四周 可判定性与不可判定性 课堂教学 第十五周 线性逻辑，时序逻辑 课堂教学 第十六周 模型检测 课堂教学 四、课程考核及说明 30%为平时成绩：平时作业(20)+课堂练习(10) 70%为期末考试成绩 五、教材与参考书 1. Anil Nerode and Richard A. Shore. Logic for Applicatio ns (2nd Editio n), Spri nger, 1997. 2. Melvi n Fitti ng. First-Order Logic and Automated Theorem Provi ng (2 nd Editi on)