基于建模与推理的命题逻辑教学方法研究

袁梦霆，李清安，吴黎兵，何炎祥

（武汉大学计算机学院，湖北 武汉 430072）

0 引言

逻辑学的研究内容涉及问题的形式化与推理，是计算机科学中的重要理论课程[1]。命题逻辑以命题为基础研究形式化与推理方法，一般是逻辑学课程的入门章节。对很多学生而言，学习命题逻辑是他们第一次接触形式化方法，再加上命题逻辑具有高度的抽象性，因此在学习过程中存在很多困难。如何激发学生对命题逻辑的学习热情，进而引导学生喜欢逻辑学与形式化方法，这是我们在逻辑学教学过程中需要解决的重要问题。

对于高度抽象的教学内容，合适的教学方法是教学成功的关键因素之一。由于命题逻辑非常抽象，在课本或者以往的相关教学研究[2-4]中往往比较重视定义、定理、命题和性质的讲解，选择的案例也是和日常生活相关的推理案例，比较偏向于数理逻辑。学生学习以后往往感觉到命题逻辑和计算机没有相关性，只能死记硬背定理，无法和计算机领域的问题关联，很难提高兴趣。

针对在传统命题逻辑教学过程中存在的问题，本文提出了基于建模与推理的命题逻辑教学方法，面向计算机专业的学生，紧密围绕命题逻辑的建模与推理内容展开教学内容，突出命题逻辑在计算机科学中的作用，提高计算机专业学生的学习效果。

1 侧重建模与推理的教学方法

为了达到良好的命题逻辑的教学效果，在讲述完命题逻辑的语法和语义之后，设计一组与计算机科学紧密相关的实例，然后向学生讲述建模的目标，引导学生对问题进行形式化建模，教导学生使用课堂讲述的自然推理法对模型的性质进行推理，最后总结与讨论建模与推理过程中碰到的问题。

1.1 案例选择

由于命题逻辑的语法非常简单，因此教师需要挑选一些不复杂但是又能代表计算机实际应用的案例。案例的设计应该考虑到覆盖命题逻辑的理论知识点，同时需要估算教学与实践的工作量，每个案例的设计按照3个学时的长度设计，使得学生能够在听完命题逻辑的理论课程后，快速通过实例掌握命题逻辑的建模与推理知识。

1.2 讲述建模目标

对于选定的建模实例，教师首先利用自然语言，撰写案例的文档，在课堂上将文档下发给每位学生。教师先讲述该实例的应用背景，阐述如何将实际的计算机应用简化为该实例。接下来教师讲述该案例的功能与需求，讲述系统必须具备的性质。通过学生的提问与讨论，保证学生对该系统具有完整与形象的了解。

1.3 形式化建模

在学生对案例有了足够的了解后，教师引导学生用命题逻辑的语法对系统进行重新描述，也就是形式化。在建模过程中，引导学生识别系统中的声明式语句与命题，体会如何使用逻辑公式描述系统规律。鼓励学生对建模过程进行开放式的讨论，对不同的模型进行对比，体会形式化过程中的优雅、简练、准确等特点。

在学生完成自己的建模工作后，教师公布参考的模型，然后与学生讨论建模过程中的心得，使得学生掌握基本的命题逻辑建模技巧。

1.4 性质推理

对于已经建好的模型，教师带领学生回顾案例的文档，列举出模型应该具有的性质，并将这些性质用命题逻辑公式描述出来，然后向学生提出问题：“如何严格证明模型具备这些性质？”在学生思考与讨论后，教师回顾课堂的“命题逻辑的语义”和“自然推演法”两种性质推理方法，让学生自行选择方法进行推理。通过性质推理，引导学生掌握基于语义和基于规则的两种推理方法，能够体会到两种方法各自的特点。

1.5 总结与讨论

在总结阶段，教师客观地对一些有代表性的学生模型进行点评，回顾建模与推理的特点与难点，同时对照命题逻辑的主要知识点进行复习，加强学生的学习效果。

最后组织学生讨论命题逻辑建模方法的缺点与限制，自然而然地引出下一章谓词逻辑的内容，激发学生的好奇心与学习兴趣。

2 教学方法应用

这里从一个案例出发，介绍如何开展以建模与推理为目的的命题逻辑教学方法。

2.1 案例描述

使用一个两位（2-bit）二进制数的加法器作为案例，该实例在计算机科学中具有普遍的代表意义，同时模型不复杂，便于学生短时间理解，使用命题逻辑就足够进行建模与推理。

使用图1对学生讲述加法器，该加法器能够将x1x0和y1y0两个二进制数相加，输出两个数相加的结果，放在z1z0中，高位的进位被舍弃。在计算过程中，x0和y0相加的结果会产生进位c，供x1和y1相加时使用。

图1 二进制加法器原理，其中z1z0=x1x0+y1y0

2.2 加法器的形式化建模

命题逻辑的建模过程分为两个步骤：（1）确定原子命题的集合；（2）使用一组命题逻辑公式描述系统的内在规律。

在本例中，我们令原子命题集合A={x0,x1,y0,y1,z0,z1,c}，其中一个原子命题a∈A成立表示变量a的值为1，否则为0。

而系统的内在规律可以用一组逻辑公式表示：P={p0,p1,…,p9}，其中p0≡(x0∧y0→c)∧(¬x0¬y0→¬c),p1≡(z0→((x0∧¬y0)(¬x0∧y0)))∧(¬z0→((x0∧y0)(¬x0∧¬y0))),p2≡c∧x1∧y1→z1,p3≡c∧x1∧¬y1→¬z1,p4≡c∧¬x1∧y1→¬z1,p5≡c∧¬x1∧¬y1→z1,p6≡¬c∧x1∧y1→¬z1,p7≡¬c∧x1∧¬y1→z1,p8≡¬c∧¬x1∧y1→z1,p9≡¬c∧¬x1∧¬y1→¬z1。

在建模的过程中，我们和学生讨论如何在此基础上简化带进位加法的性质描述。

2.3 加法器的性质推理

在学生理解加法器模型之后，我们引导学生验证模型的性质。在本例中，我们假设要验证01+10=11。首先，我们引导学生对这个性质进行形式化，也就是用命题逻辑的sequent来表示该性质：P,x0,¬x1,¬y0,y1z0∧z1。然后鼓励学生采用自然推演法来证明该sequent是有效的。

该性质的自然推演法证明过程如下（限于篇幅，该证明过程中合并了一些显而易见的小过程）：

讲解推理过程，帮助学生体会推理过程的严谨性，了解自然推演法的使用技巧，进而灵活运用自然推演法。

2.4 讨论

在与学生讨论的过程中，我们主要注意引导学生对以下内容的思考：（1）命题逻辑的语法非常简单，所以导致了模型性质描述很繁冗，问学生有什么方法可以增加命题逻辑的建模复杂度。提示学生考虑在命题逻辑的基础上利用恒等式扩充语法。（2）在本例中，我们只证明了系统满足01+10=11一个特定的性质，可以引导学生思考如何推理所有二进制数加法的性质，进而引出谓词的概念，从而将学生引入下一章的谓词逻辑的话题，激发学生对课堂新任务的期待与热情。

3 结语

实践表明，针对计算机科学相关的实例，利用命题逻辑对其进行建模与性质推理，能够帮助学生更扎实地掌握命题逻辑的知识点，并且直观的了解形式化的过程与技巧，充分调动了学生对逻辑学的学习兴趣，同时让学生不再惧怕抽象的逻辑概念，能够理论联系实际，有利于后续章节的学习。