常 亮，徐周波，孟 瑜，古天龙
（桂林电子科技大学计算机科学与工程学院，广西桂林541004）
摘要：针对离散数学课程中的数理逻辑教学，分析计算思维与数理逻辑之间的内在关系，从计算思维的角度对数理逻辑教学内容进行梳理，论述如何将“对问题进行抽象建模一形式化一自动化一分析评估”这一思维模式贯穿于教学过程中，以及如何在教学中强调计算思维的基本概念和基本方法。
教育期刊网 http://www.jyqkw.com
关键词 ：计算思维；数理逻辑；抽象；形式化；自动化
文章编号：1672-5913(2015)15-0031-05
中图分类号：G642
第一作者简介：常亮，男，教授，研究方向为知识表示与推理、形式化方法，changl@guet．edu．cn。
0 引 言
对计算思维能力的培养已经成为新一轮大学计算机课程改革的核心导向。如何从计算思维的角度重新梳理和组织计算机相关课程的教学内容，如何在教学实施中培养学生的计算思维能力，是近年来计算机教育者热烈探讨的问题。
数理逻辑是计算机专业核心基础课程离散数学中的主要教学内容，不仅为数据库原理、人工智能等专业课程提供必需的基础知识，更对培养学生的抽象思维能力和逻辑思维能力起着重要作用。
1 计算思维
计算思维运用计算机科学的基本概念来求解问题、设计系统和理解人类行为，包括一系列广泛的计算机科学的思维方法。根据卡内基·梅隆大学周以真( Jeannette M．Wing)教授的设想，一个人具备计算思维能力体现在以下几个方面：给定一个问题，能够理解其哪些方面是可以计算的；能够对计算工具或技术与需要解决的问题之间的匹配程度进行评估；能够理解计算工具和技术所具有的能力和局限性；能够将计算工具和技术用于解决新的问题；能够识别出使用新的计算方式的机会；能够在任何领域应用诸如分而治之等计算策略等。在计算思维所包含的诸多内容中，最根本的内容是抽象和自动化。
在计算机专业相关课程的教学中，为了培养学生的计算思维能力，我们认为一种有效的途径是从问题出发，抓住抽象和自动化这两个核心内容，培养学生分析问题、解决问题和对解决方案进行评估的能力。同时，我们提炼出计算机学科以及各门具体课程中涉及的基本概念和思维方法，在教学过程中有意识地强化学生对这些基本概念和思维方法的理解和掌握。
2 基于计算思维的数理逻辑数学内容组织
数理逻辑应用数学中的符号化、公理化、形式化等方法来研究人类思维规律。从广义上看，数理逻辑是数学的一个分支，包括证明论、集合论、递归论、模型论以及各种逻辑系统等5部分。我们在这里谈的是狭义的数理逻辑，即大学计算机相关专业学习的数理逻辑基础。
数理逻辑与计算机科学有着非常密切的关联。无论是在ACM和IEEE-CS联合攻关组制订的《计算教程CC2001》中，还是在中国计算机学会教育委员会和全国高等学校计算机教育研究会联合制定的《中国计算机科学与技术学科教程2002》中，数理逻辑都是计算机相关专业的核心知识单元。对于计算机相关专业来说，数理逻辑的教学内容主要是命题逻辑和一阶谓词逻辑这两个基础的逻辑系统。针对这两个逻辑系统，传统的教学大纲主要从语法、语义、等值演算、形式证明系统等4个方面安排教学。在开展教学的过程中，教师强调的主要是培养学生的抽象思维能力和逻辑思维能力。然而，从学生的角度看，这两种能力本身都是抽象的口号，处于大一或者大二阶段的学生难以将这些知识点与计算机科学联系起来，感觉不到数理逻辑在计算机科学或者将来工作中的具体应用，从而缺乏相应的学习兴趣。
数理逻辑中的许多思想都与计算思维有着异曲同工之妙；最为明显的是数理逻辑和计算思维都强调抽象及形式化。在关于离散数学课程的教学实践中，我们已经把计算思维的诸要素或多或少地渗透到包括数理逻辑在内的培养方案和教学大纲中，但尚未上升到以培养计算思维能力为导向的高度。
在明确将培养计算思维能力作为一个新的教学目标之后，我们从计算思维的角度对数理逻辑教学内容重新进行梳理。具体来说，在计算思维的指导下，我们以问题求解作为出发点，抓住抽象和自动化这两个核心内容，按照“对问题进行抽象建模一形式化一自动化一分析评估”的主线来组织数理逻辑教学，培养学生应用计算思维分析问题和解决问题的能力。与此同时，在教学实施的过程中，尽可能地提炼出各个知识点中关于计算思维的基本概念和基本方法，把计算思维贯彻到每堂课中。
2.1 从问题出发引入数理逻辑
在传统的数理逻辑教学中，开篇的内容就是对命题进行符号化，但许多学生并不清楚为什么要进行符号化。在计算思维的引导下，我们可以通过如下两个问题来引人数理逻辑。
第一个问题是莱布尼茨创立数理逻辑时的理想：把推理过程像数学一样利用符号来描述，建立直观而又精确的思维演算，最终得出正确的结论。形象地说，当两个人遇有争论时，双方可以拿起笔说“让我们来算一下”，就可以很好地解决问题。为了实现莱布尼茨的理想，基本思路是首先引入一套符号体系，将争论的内容严格地刻画出来；其次规定一套符号变换规则，借助这些符号变换规则，将逻辑推理过程在形式上变得像代数演算一样。
第二个问题是人工智能中的知识表示和知识推理。人工智能中的符号主义学派认为，人的认知基元是符号，认知过程就是符号操作过程；知识可以用符号表示，也可以用符号进行推理，从而建立起基于知识的人类智能和机器智能的统一理论体系。基于这种思路，为了在计算机上实现智能，我们首先需要将知识用某套符号体系表示出来，然后在此基础上通过算法进行知识推理，最终实现智能决策等一系列体现智能的功能。
从上述两个问题出发，我们可以将命题逻辑和一阶谓词逻辑当作两个工具来引入。与此同时，对于这两个工具来说，应用它们来解决问题的过程又可以被分解为符号化表示和符号化推理两个阶段。因此，我们最终可以从两个维度上引入数理逻辑：一个维度是命题逻辑和谓词逻辑两个工具，另一个维度是符号化表示和符号化推理两个过程。与传统的直接介绍数理逻辑形式系统的方式相比，这种从问题出发的引入方式与计算机专业学生的思维方式即计算思维一致。
2.2 从形式化的角度组织教学内容
作为彻底的形式系统，数理逻辑为培养计算思维中的抽象思维能力提供了非常好的素材。从形式系统自身的角度来看，我们还可以将语法和语义两个内容独立出来。在此基础上，我们用表1对计算机相关专业数理逻辑部分的学习内容进行概括。
表1列出的知识点与《计算教程CC2001》《中国计算机科学与技术学科教程2002》中关于数理逻辑的知识点一致。借助这张表，可以让学生对数理逻辑部分的学习内容形成一个清晰、全面的认识。在教学过程中，每开始一个新的章节，我们都可以呈现这张表，帮助学生知道接下来的学习内容处于哪个位置，并且加深他们对计算思维中抽象和建模的印象。
需要指出的是，在广义的数理逻辑中，介绍形式演算系统时通常是指公理推理系统。公理推理系统从若干条给定的公理出发，应用系统中的推理规则推演出系统中的一系列重言式。公理推理系统可以深刻揭示逻辑系统的相关性质以及人类的思维规律，但从计算思维解决问题的角度来看，我们并不关注公理推理系统。在知识推理中，我们关注的是从任意给定的前提出发，判断能否应用推理规则推演出某个结论；我们并不要求这些前提和结论是重言式。因此，对于计算机专业的数理逻辑来说，我们关注的是自然推理系统，即构造证明法。计算思维为我们选择自然推理系统而不是公理推理系统提供了一个很好的视角。
2.3 在数理逻辑中强调自动化
表1的知识点充分体现了计算思维中抽象和对问题建模求解的思维方式，但计算思维中的自动化尚未体现出来。在学习了构造证明方法之后，学生一般会形成一个印象，认为构造证明法使用起来简单方便，与人们的直观逻辑思维一致，但使用过程中需要一定的观察能力和技巧。与之相反的是，计算思维希望能够通过算法实现问题的自动求解。
实际上，在广义的数理逻辑中已经存在许多自动化证明方法，其中最为典型的是归结推理方法和基于Tableau的证明方法。为了判断能否从给定的前提推导出某个结论，我们同样可以采用归结推理方法或者基于Tableau的证明方法。具体来说，我们首先对拟证明的结论进行否定，将该否定式与所有前提一起合取起来，然后判断所得到的合取式是否为可满足公式；如果不可满足，则表明可以从给定的前提推导出结论，否则表明所考察的结论是不能得出的。换句话说，前提与结论之间是否可推导的问题被转换为公式可满足性问题来解决。
归结推理方法最早于1965年由Robinson提出，是定理证明中主流的推理方法。《计算教程CC2001》和《中国计算机科学与技术学科教程2002》都将其列为人工智能课程的一个重要知识点。由于许多学校都是将人工智能作为选修课来开设，因此许多学生都没有机会接触和学习。实际上，在数理逻辑的教学实践中，只需要很少的课时就可以把归结推理方法讲授清楚。具体来说，在讲授完构造证明法中的归谬法之后，只需要补充介绍归结原理这一条推理规则就可以了，最多只花费半个课时。当我们用简洁的算法把归结推理方法描述清楚，让学生直观感受到机械化的证明过程之后，学生对计算思维就有了更进一步的认识和掌握。在有条件的情况下，还可以让学生上机实现命题逻辑的归结推理算法。
基于Tableau的证明方法出现的时间早于归结推理方法，最初在1955年就被Beth和Hintikka分别独立提出，之后Smullyan在其1968年出版的著作中进行了规范描述。Tableau方法的基本思想是通过构造公式的模型来判断公式的可满足性。虽然Tableau方法使用的推理规则不只一条，但每条推理规则都直观地体现了逻辑联结词的语义定义。Tableau方法在早期没有受到太多关注，但最近十多年来，随着描述逻辑成为了知识表示和知识推理领域的研究热点，在描述逻辑推理中发挥出优异性能的Tableau方法得到了越来越多的关注。鉴于此，在讲授完构造证明法和归结推理方法之后，我们也向学生简单描述了Tableau方法，引导学有余力并且对学术前沿感兴趣的学生在课后自学。
2.4 在分析评估中强化计算思维
在讲授数理逻辑的过程中，我们还可以从许多知识点提炼出计算思维的内容，把计算思维贯彻到每个具体的教学内容中。我们列举体现计算思维的4个典型内容进行探讨。
首先，命题公式和谓词公式的语法定义为计算思维中的递归方法提供了经典案例。实际上，除了公式的语法定义外，数理逻辑中在对语义的定义、对语法与语义之间关系的研究、对算法正确性的证明、对算法复杂度的分析等各项内容中都用到了递归。由于课时的限制，我们不能在数理逻辑教学中对其展开，但可以点出这个情况，让将来可能继续攻读硕士或博士学位的学生留下一个印象。
其次，当我们讲授了用归结推理方法或者Tableau方法进行自动推理和问题求解之后，从计算思维的角度看，一个很自然的想法是想知道这种解决方法的求解效率。因此，我们可以对命题逻辑中推理算法的复杂度进行分析。由于我们已经把归结推理方法通过非常简洁的算法呈现在学生面前，因此只需要进行简单的口头分析就可以得出最坏情况下的算法复杂度，让学生知道命题逻辑的公式可满足性问题是NP问题。到此为止，在对命题逻辑进行讲授的过程中，我们引导学生完成了“对问题进行抽象建模一形式化一自动化一分析评估”的完整流程。如果在后继课程中再反复重现这个流程，将可以把这种思维模式固化到学生大脑中，使得计算思维成为他们日后解决新问题的有效工具。
第三，在讲授完命题逻辑之后，我们可以用著名的苏格拉底三段论作为例子来引入谓词逻辑。首先我们用命题逻辑对“所有的人都是会死的”“苏格拉底是人”“苏格拉底会死的”进行符号化，然后展示在命题逻辑下无法从两个前提推导出后面的结论，从而说明命题逻辑在表达能力上的局限，进而阐述引入一阶谓词逻辑的原因和思路。从计算思维的角度看，这个过程体现了如何选择合适的表示方式来陈述一个问题，以及如何确定对问题进行抽象和建模的粒度，此外，这个例子还让学生直观感受到了计算工具所具有的能力和局限性。
最后，在讲授完一阶谓词逻辑的推理之后，我们可以介绍一阶谓词逻辑的局限，即一阶谓词逻辑是半可判定的，一阶谓词逻辑的归结推理算法不一定终止。从计算思维的角度看，这个结论给了我们一个很好的例子，可以引导学生分析哪些问题是可计算的，哪些问题是不可计算的。在此基础上，我们进一步阐述逻辑系统的表达能力与推理能力之间存在的矛盾关系：一阶谓词逻辑在表达能力上远远超过命题逻辑，但其推理能力仅仅为半可判定；命题逻辑可判定，但描述能力不强。从计算思维的角度看，此时我们可以引入“折中”这个概念，训练学生在解决问题的过程中抓住主要矛盾，忽略次要矛盾。更进一步地，我们向学生简单介绍目前作为知识表示和知识推理领域的研究热点的描述逻辑：早期的描述逻辑通常被看做一阶谓词逻辑的子语言，在表达能力上远远超过命题逻辑，但在推理能力上保持了可判定性。这些补充内容既能让学生接触到学科前沿，又能帮助学生深刻理解如何根据问题的主要矛盾来选择合适的工具。
3 结语
总的来说，数理逻辑很好地诠释了计算思维并为其提供了生动的案例。将数理逻辑的教学与计算思维培养结合起来，一方面可以从计算思维的角度重新审视和组织数理逻辑的课堂教学，取得更好的教学效果；另一方面能加强对计算思维能力的培养，使学生能够更好地应用计算思维来解决问题。
计算思维的培养不是通过一两门课程的教学就能解决的问题，而是应该贯穿于所有的专业课程教学中。要实现这个目标，要求授课教师不仅仅照本宣科以教会学生课本上的知识为目的，而要能够从计算思维的高度来看待所讲授的课程，对所讲授的课程中含有的计算思维基本概念、方法和思想不断进行提炼，从计算思维的角度对课程进行重新梳理和建设。进行教学改革的目标是要更好地培养学生的计算思维能力，在实施教学改革的过程中，授课教师的计算思维能力也得到不断的提升和加强。
教育期刊网 http://www.jyqkw.com
参考文献：
[1]教育部高等学校大学计算机课程教学指导委员会．计算思维教学改革宣言[J]．中国大学教学，2013(7): 7-10．
[2]李廉，以计算思维培养为导向深化大学计算机课程改革[J]．中国大学教学，2013(4): 7-11.
[3]常亮，徐周波，古天龙，等，离散数学教学中的计算思维培养[J]．计算机教育，2011(14): 90-94.
[4]丁金凤，李英梅，徐建山，等．基于计算思维的程序设计类课程教学实践[J]．计算机教育，2012(15): 65-68．
[5]周虹，傅向华，王志强，等．基于计算思维的计算机图形学教学改革[J]计算机教育，2013(5): 55-58．
[6]李文生，吴舜歆．面向计算思维能力培养的程序设计课程[J]计算机教育，2014(3): 57-60．
[7] Jeannette MW. Computational thinking [J]. Communications ofthe ACM, 2006, 49(3): 33-35.
（编辑：郭田珍）
