What:数理逻辑是数学的一个分支,是数学基础的一个不可缺少的组成部分.数理逻辑的研究范围是逻辑中可被数学模式化的部分.数理逻辑的研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统.(from Wikipedia)

Who: 秦逸(南京大学仙林校区计算机科学与技术系楼501室;)

Where:仙林校区逸B-212

When:每周五2-4节(09:00 - 12:00),1-16周

Which:《数理逻辑十二讲》, 宋方敏、吴骏著,机械工业出版社(请注意选择第二次印刷的版本)。教材的电子版本和对应勘误表已在本网站发布(仅供个人使用,版权归属作者和出版社).

Why:数理逻辑的研究孕育了计算机科学.除了理论计算机科学之外,数理逻辑或基于数理逻辑的研究成果,对编程语言、软件系统理论和人工智能理论都产生了巨大而深远的影响。数理逻辑课程中所展现的,对计算过程的形式化定义、描述和证明方法,被广泛地应用于计算机领域的学术研究中.


课程规则

课程平时成绩占总成绩的10%,期中作业占总成绩的20%,期末考试成绩占总成绩的70%.

平时成绩主要由作业提交情况决定.

期中作业会在第五章教学结束后进行,形式为课后习题,主要考察前四章介绍的关于数理逻辑的基本概念和基本方法,难度会显著低于课后作业.

期末考试会在学期结束后进行,形式为开卷考试,主要考察课程讲述的关于数理逻辑的基本方法和基本技巧,难度会显著低于课后作业.


动态新闻

2024-03-22:第一次作业上传

2024-03-22:第三讲相关材料上传

2024-02-29:第一次课程相关材料上传

2024-02-26:课程教材及勘误上传

2024-02-26:课程主页建立,散花


课程讲义

一般上课前给出,但可能随时会更新,注意看更新时间,以确保自己下载的是最新版


书面作业

课程邮箱为mathlogicnju at 163.com, 提交时请将邮件主题设为“学号+姓名+第XX次作业”。提交时可以提交1)电子版作业;2)手写作业的照片,但请注意提交版本的清晰度。


补充材料

本课程的书面作业涉及到大量数学公式的表示和排版。推荐大家使用科技排版系统LaTex完成并提交电子版本的书面作业。LaTex是由图灵奖得主Leslie Lamport设计并开发的一种排版系统,在今日的学术论文撰写中有着不可替代的重要作用。这里是其中文版本CTex的下载地址。

参考书目选择: 由于课程教材主要侧重于数理逻辑原理、方法的数学表示,给同学们在课余时间的教材阅读、理解带来了一定的难度。同学们可以自由选择下列参考书籍作为辅助,以帮助理解教材中所列的数学表示之后的原理。

  • 《数理逻辑-基本原理与形式演算》, 李未 著, 科学出版社。该书不仅涵盖了经典数理逻辑的核心内容,也阐述了李未教授长期以来将数理逻辑原理应用于软件工程理论的思考和实践。需要特别指出的是,有别于传统的、基于数学思维方式的方法,该书采用了计算机软件的思维方式来描述、解释数理逻辑中的基本概念和方法,增加了经典概念的可读性和可解释性。

  • Logic in Computer Science, M. Huth & M. Ryan 著,Cambridge University Press。该书从计算机科学的实践角度,通过模型验证,多Agent系统,和二分决策图三个例证,系统性地展示了数理逻辑原理和计算机科学实践的结合过程和结果。

  • A First Course in Logic, S. Hedman 著, Oxford University Press。该书从可计算性的角度,系统性地介绍了从命题逻辑到NP问题的一系列数理逻辑基础概念和经典结论。

    关于数理逻辑证明

    本课程中的大多数问题都会要求您“证明”某事,即给出令人信服的解释为什么这件事是真的。为了增加您做期中作业/期末试卷中所给证明获得相应分数的机会(我们会在后面解释为什么是“机会”),您的证明至少应该看起来像教科书中的证明,尤其做到:

  • 通过完整的、语法正确的句子组成您的证明;

  • 证明中出现的所有变量要么出现在被证明的陈述中,要么在证明中的某处通过使用“设/令/let”等元语明确引入;

  • 每个陈述要么清楚地、合乎逻辑地遵循先前的陈述(并解释该逻辑),要么以明确的目的引入(例如“假设矛盾...”或“归纳假设是...”);

  • 任何未被证明的东西都被引用,通过它的通用名称(例如算术基本定理)或参考我们的教科书(例如第XX页的命题XX/定理XX);

    证明的目的不是向评分者说明您理解问题中的想法,而是向具备相应数学/逻辑学基础,但是没有考虑过这个特定问题的其他人解释您进行推理和论证的方案。而在这个过程中,您只能写给他们,而不是说话。鉴于此:

  • 老师在讲课时写在黑板上的东西不构成书面证明,因为这些板书脱离老师说的东西就毫无意义;

  • 证明的评判标准在于评分者能否在预设前提下,仅仅通过书面文字就理解您的推理过程。因此老师难免会出现难以理解某些证明步骤的情况(即便这些步骤在您看来可能就像费马证明费马猜想一样精妙)。为了防止这种情况发生,在期中作业/期末考试后,您可以就您的分数提出异议,并来与老师一起进行证明的审查。