数理逻辑教学方法探讨

李志敏,夏学文,张学敏

(孝感学院计算机与信息科学学院,湖北孝感432000)

数理逻辑教学方法探讨

李志敏,夏学文,张学敏

(孝感学院计算机与信息科学学院,湖北孝感432000)

数理逻辑不仅是离散数学课程的基础,也是计算机科学与技术专业其他课程学习的重要基础。文章就如何提高数理逻辑的教学质量,提出了注重教学内容的合理拓展与延伸、注重数理逻辑在计算机科学与技术领域应用背景的介绍、注重引入先进教学资源和教学辅助工具(如ProofWeb)等教学方法。

离散数学;数理逻辑;计算机科学与技术专业;ProofWeb

离散数学是现代数学的一个重要分支,是计算机科学中基础理论的核心课程。离散数学通常研究的领域包括数理逻辑、集合论、代数结构、关系论、函数论、图论、组合学、数论、形式语言与自动机理论等,它是高校计算机及相关专业的重要基础课程之一。学习离散数学,可以培养和提高学生的抽象思维能力和逻辑推理能力,为学生继续学习和工作以及参加科学研究打下坚实的数学基础[1]。

数理逻辑是离散数学课程的重要基础,它是用数学方法来研究推理的形式结构和推理规律的数学学科。数理逻辑的主要分支包括逻辑演算(包括命题演算和谓词演算)、模型论、证明论、递归论和公理化集合论,它与数学的其他分支、计算机科学、人工智能、语言学等学科均有十分密切的联系,并且日益显示出它的重要作用和更加广泛的应用前景。

近来,各高校非常重视数理逻辑的教学,例如,复旦大学着眼于高起点,用泛代数术语讲授命题逻辑和谓词逻辑直到完备性、可靠性以及推理,取得优良的教学效果[2]。上海交通大学用一个学期专门讲授数理逻辑,给学生打下了坚实的理论基础,提高了后续学习能力。

在实际教学中,多数院校数理逻辑授课时间仅有20多个课时,因而教学内容不断精减,造成学完这部分知识后,学生感觉不能满足需要。而对数理逻辑的把握程度将直接影响到学生对后续专业课程的学习,影响到学生计算机思维逻辑的正确形成。提高本科数理逻辑的教学水平和质量,对学生学习后面的内容具有现实的意义。本文就如何提高数理逻辑的教学质量,从三个方面进行了探讨。

1 教学内容合理拓展与延伸

1.1 从全面了解数理逻辑理论体系的角度延伸教学内容

任何逻辑都有两个重要层面:语义(semantics)和语法(syntax,也可以称作是proof theory或proof systems)。研究逻辑一般从语义、语法以及二者之间的联系三个方面展开。由于授课时间的限制,普通本科生教材通常只介绍语义,较少介绍语法(有的教材叫做形式证明或证明技术),基本不讲语义和语法之间的联系。这种处理方式对少学时培养方案而言,不失为是一种选择。实践证明,这种处理显得较为粗糙,不利于学生掌握知识的完整体系和后续学习能力的培养。我们在教学中需要补充适当的教学内容,要让学生全面认识数理逻辑理论的体系[3-4]。为此,我们的做法是在学完命题逻辑部分后,按以下几个层次全面小结命题逻辑:

1)语法。命题逻辑的形式系统是由命题变元符号、逻辑符号、由这些符号形成合式公式的规则、由若干公式组成的公理、由公理经一定的法则得到的定理所组成。形式系统的语法就是从公理(或一组公式集)出发的证明。

2)语义。包括命题的真值、联结词的意义、命题公式真值、永真式(逻辑等价式和逻辑蕴涵式是永真式的特例)。利用一些基本的逻辑蕴涵式、逻辑等价式以及代入、替换规则,通过代数变换,导出更多的逻辑蕴涵式、逻辑等价式,是这一层面的核心内容。这部分的教学,要使学生对思维的规律有更清楚的认识,对逻辑的数学属性有更深刻的了解,并能利用代数变换进行语义层面的逻辑推导,从一些前提出发,导出它们的逻辑结果。

3)语义与语法的联系。这一部分主要介绍命题逻辑的可靠性定理(命题公式是定理,那么一定是永真式),命题逻辑的形式系统是和谐的(存在公式不是定理),命题逻辑的形式系统的完全性定理和紧致性定理,命题逻辑公式类是可判定的(存在一个算法判定任一命题公式是否是定理)。

最重要的逻辑是一阶逻辑,它是任何逻辑的基础,它的表达能力很强并且具有良好的性质(例如完全性和紧致性)。学好一阶逻辑是进一步学习的必备基础。在讲授谓词逻辑时,我们首先引导学生类比命题逻辑理论体系构建谓词逻辑形式系统的基本理论框架,然后让学生利用课外时间查阅资料,从语义、语法及二者之间的关系等三方面预习课本知识,证明相关结论。教学实践证明,上述办法能较好地提高学生自主学习的积极性。

1.2 从经典逻辑到非经典逻辑理论的角度拓展教学内容

经典逻辑是指由弗雷格、皮尔士、罗素等人创立的现代逻辑系统,由统一的命题演算和谓词演算构成,叫做“一阶逻辑”,其特点是使用特定的人工符号语言,运用公理化、形式化的方法。经典逻辑是研究最深入和使用最广泛的一类形式逻辑。它们具有如下特征:排中律、无矛盾律、蕴涵的单调性和蕴涵的幂等性、合取的交换性、De Morgan对偶性。

经典逻辑的局限性表现在不适合于非直谓性推理、不确定性推理以及内涵性推理,特别是经典逻辑中存在蕴涵怪论和逻辑悖论等无法解决的异常现象和悖论[5]。

在引入非经典逻辑的过程中,要注意讲明非经典逻辑对经典逻辑的发展,以及如何克服经典逻辑的局限性。

计算机科学与人工智能的需要,促使非经典逻辑的理论与应用研究持续发展。一类非经典逻辑是在经典逻辑基础上的拓展。模态逻辑、时态逻辑、道义逻辑等都属于这一类系统。它们保留经典逻辑原有的基本公理、推理规则和基本算子。例如,模态逻辑就是在经典一阶逻辑的基础上,增加“可能”、“必然”等算子。如果增加“应该”、“允许”、“禁止”等算子就称为道义逻辑,而时态逻辑则是增加“过去”、“现在”、“将来”等算子。

另一类非经典逻辑是对经典逻辑系统进行修改或限制而得到的,如直觉主义逻辑、多值逻辑、模糊逻辑、次协调逻辑和相干逻辑等等。这种非经典逻辑可以处理经典逻辑无法解决的异常现象。例如,为了逻辑系统解决逻辑系统中的“实质蕴涵怪论”,阿克曼创立了相干逻辑。

在引入非经典逻辑时,要以学生现有知识和容易观察到的现象为背景。我们在讲授相干逻辑时,从课本例题出发。例如命题“如果太阳从西边出来,那么长江流经武汉”,其内容上毫不相干,逻辑值却是真的。对这样的蕴涵式,引导学生发现经典逻辑的实质蕴涵有弊端。为了避免实质蕴涵的弊端,逻辑学家提出了一条基本原则:蕴涵式A→B的前提A和结论B至少包含一个共同的变元时,公式A→B才是合理的。由此可知,在相干逻辑系统中,如下公式都是无效的:

⇁P→(p→q),(⇁pΛp)→q,p→(p→q)

教学实践证明,以教材知识为基础,适时将经典逻辑进行拓展,引入非经典逻辑,讲清楚非经典逻辑的来龙去脉,理清各种逻辑系统的联系与区别,就能帮助学生理解逻辑系统的构造,提高学生学习兴趣。

2 数理逻辑应用背景知识介绍

逻辑的概念、结论和方法在计算机科学中的地位越来越重要,它是人工智能、程序描述与验证、形式语言、自动定理证明和算法理论的重要工具。一般说来,计算机科学中逻辑的作用有两个方面:一是服务于计算机科学研究领域的基础;二是逻辑的语言和演算是软件开发、数据库系统和知识表示的工具。在这些方面应用,已有不少的文章作介绍。我们认为数理逻辑在如下领域的应用值得让本科学生了解:

1)自动定理证明。关于这一领域,适宜于介绍王浩算法、D-P过程、Robinson归结方法。

2)逻辑编程。逻辑编程起源于归结证明过程,仅用Horn子句就特别有效。人们发现Horn子句不仅描述了输入和输出关系,而且还给出了算法,于是产生了使用逻辑作为编程语言的想法。算法重新表达为:算法=逻辑+控制。

逻辑编程语言是一个证明程序,即证明系统和搜索策略。逻辑编程中最有意义的一个问题是:逻辑的哪一部分可以看作是编程语言?

关于逻辑编程,可以结合PROLOG讲授,让学生学会使用PROLOG,解决简单的应用问题。

3)程序验证。程序验证是研究使用形式化方法,严格证明一个程序符合其预定目标,因而是正确无误的。目前验证还处于初级阶段,近几十年来,尽管各种各样的验证工具不断地被研制出来,但只能作到程序不同程度地被验证。

限于学生的知识能力和接受水平,仅简单介绍基于逻辑推理的验证。这是说明逻辑在计算机科学中应用的有用素材。这种方法将程序验证转换为逻辑推理问题,首先要建立合适的逻辑系统,用以描述程序。本科教学中,介绍最著名的Hoare逻辑,与其他逻辑系统比较,该逻辑系统容易让学生接受。

基于Hoare逻辑的程序验证方法的基本思想是对高级语言中的每一种基本控制结构(如条件语句、循环语句)都可以有相应的推理规则,要证明整个程序的正确性,就是使用这些推理规则进行推导。从理论上讲,这种方法非常强大,能证明各种程序的正确性。它的不足之处是要求使用者具有较高的专业水平,比如能给出循环不变式。另外,还要求有表达力非常强的定理证明器,而这些定理证明器目前很难自动化。

程序验证的教学中,不要超过让学生了解应用逻辑解决实际问题的方法这个层次,主要目的还是激发学生学习的兴趣。

3 基于ProofWeb的数理逻辑教学系统

数理逻辑的教学,离不开网络资源的辅助。在此我们介绍基于ProofWeb的数理逻辑教学系统,它是由Cezary Kaliszyk和Freek Wiedijk等人于2006年开发完成的“计算机辅助逻辑教学系统”[6]。

数理逻辑是计算机科学与技术专业本科以及研究生阶段的基础课程。它的两个最基本,也是最重要的组成部分是“命题演算”和“谓词演算”。在数理逻辑的学习过程中,练习是关键的活动之一,常常出现一些学生不能判断近似正确但并不是完全正确的证明,虽然学生也可以使用一些计算机程序,引导他们发现完全正确的证明,而这样做的一个缺点是学生可能会偶然得到解题方法,但并不真正理解证明过程。实践证明将传统方式和计算机程序引导相结合的方式是最好的选择。

3.1 ProofWeb系统简介

ProofWeb系统具有如下两个优势:

第一,该系统必须通过一个网络界面,使学生在中央服务器上进行学习过程,证明助手不在学生的电脑上运行,而是在服务器上运行。这种架构的第一个好处是学生不需要安装任何软件,他们可以从任何电脑经过互联网连接使用,不受地域和时间的限制;第二个好处是学生不需要考虑软件的版本问题,由于一切都是在同一个中央服务器上,学生们在任何时间可以得到软件的授权版本,练习题目及其可能解答,老师也可以在任何时候知道学生的学习状况。

第二,该系统充分利用了最先进的证明助手,即Coq。该系统成功验证了著名的四色定理和C语言编译器等数学和计算机科学相关理论和应用课题。

Cezary Kaliszyk和Freek Wiedijk等人开发的ProofWeb系统增加了如下功能模块:

1)备有大量的逻辑练习题,设置的难度级别涵盖了非常容易到非常难,学生不会很快就可以完成全部练习。

2)课程介绍和使用说明书,系统提出的证明与教科书同步,系统开发了Gentzen-型和Fitch-型两个自然演绎变种。

ProofWeb系统突出的特点是该系统使用严谨的证明助手和基于Web应用程序架构,学生学习情况保留在Web服务器上,学生本人、老师和系统可以随时了解学生学习进展。

3.2 ProofWeb使用方法介绍

ProofWeb系统既能用于逻辑教学又能作为证明助手。ProofWeb用户有3种登陆方式:第一,不需要注册登录;第二,如果是学习逻辑或证明助手课程的学生,系统提供免费课程,如果是教师用户,并希望在此服务器上进行教学,可发送邮件至proofweb@cs.ru.nl联系;第三,教师还可以下载ProofWeb系统并在自己的服务器上运行。

具体操作步骤如下:

1)进入网页http://prover.cs.ru.nl/,注意ProofWeb不一定在所有的浏览器上运行正常,在Firefox上一般没问题。

2)在靠近页面的底部点击课程名称。

3)输入用户名和密码。

4)按一下你想工作的问题的按钮。

5)可以选择Debug菜单上的项目Toggle E-lectric Terminator,这样每输入一个‘.’时,命令自动执行,否则将需要按向下箭头或输入controldown执行命令。

6)点击向下箭头或输入control-down,直到已经执行了定理行后面的证明行。现在,开始进行证明工作。这时,不完整版本的证明会显示在右下角。

7)用下一页描述的一系列策略取代(＊!prop_proof＊)的注释。如果您没有做第5步的Toggle Electric Terminator,那么需要反复按向下箭头(或输入control-down)执行证明策略。

8)用户也可以从模板、向后和向前的菜单选择输入策略项目,用标签、公式和项取代问号(‘?’),这样做之后,按一下向下箭头或输入control-down。

9)用户可以修改尚未被处理的部分文字(已被处理部分将变成绿色),若要撤消证明步骤,点击向上箭头或输入control-up。

10)如果用户有关于ProofWeb的问题,或交流经验,可以使用ProofWeb形式的课程讨论板。

应用ProofWeb系统进行教学,可以培养学生自主学习能力,减少教师批阅学生证明练习的时间。成功开发系统ProofWeb,也是数理逻辑的一个典型应用案例。

4 结束语

本文针对数理逻辑教学中存在的问题,提出了一些教学建议,经在孝感学院计算机科学与技术专业离散数学课程教学实践中运用,效果较好,主要表现在学生学习兴趣不断增强,提高了学生自主学习能力,培养了研究型学习习惯。

[1] 屈婉玲,耿素云,张立昂,等.离散数学[M].北京:高等教育出版社,2008.

[2] 朱洪.离散数学教程[M].上海:上海科学技术文献出版社,1996.

[3] 王元元.计算机科学中的现代逻辑学[M].北京:科学出版社,2002.

[4] 王元元,陈卫卫,贺汛.离散数学数理逻辑教学中值得关注的几个问题[J].计算机教育,2009(16):136-138.

[5] 王辉.逻辑理论变革的必然趋势[J].辽宁工学院学报,2003,5(2):36-37.

[6] Cezary Kaliszyk,Freek Wiedijk.Teaching logic using a state-of-the-art proof assistant[C]//Proceedings of PATE’07.Elsevier,2007.

Abstract:Mathematical logic is a foundation of discrete mathematics and also an important basic knowledge for learning in computer science and technology speciality.In this paper,for the purpose of improving teaching quality of mathematical logic,the authors proposed teaching approach from the aspects of focusing on the reasonable extending of teaching content,introducing applications-oriented background knowledge and the advanced teaching resources and aided teaching tools such as Proof-Web.

Key Words:discrete mathematics;mathematical logic;computer science and technology speciality;ProofWeb

On the Teaching Approach of Mathematical Logic

Li Zhimin,Xia Xuewen,Zhang Xuemin
(School of Computer and Inf ormation Science,Xiaogan University,Xiaogan,Hubei432000,China)

G642.41

A

1671-2544(2010)03-0105-04

2010-04-06

李志敏(1967— ),男,湖北云梦人,孝感学院计算机与信息科学学院讲师,博士。

(责任编辑:张晓军)