命题逻辑中形式推演证明题的自动评阅系统

魏 玮，谢慧珍，张丽纯

(河北工业大学计算机科学与软件学院，天津 300401)

0 引言

面对越来越多的学生和高负荷的阅卷工作，教师要完全细致地评阅试卷是件很困难的事。因此计算机自动阅卷系统的出现有其必然性。对于客观题，评分一般采用简单的匹配算法，实现起来比较容易;而主观题部分由于操作的多样性、复杂性和不确定性使其评分的实现难度骤升。现阶段对主观题的研究大部分都致力于文字类主观题［1-2］，对数学类主观题自动评阅的研究比较少。

国内相关的研究成果有李兵在其博士论文中实现了初等代数证明题答案的自动化检测［3］和杨宁学设计实现了基于材料力学的计算类主观题的自动评阅系统［4］。数理逻辑是数学的一个分支，关于这方面吴文俊和张景中院士早在几年前就对符号运算、公式翻译和机器证明技术进行了富有丰硕成果的研究，成功地解决了计算机的自动推理问题，其重在开发计算机的自动推理和自动求解的能力，让计算机能够自动完成代数式的化简和恒等变换，或者是几何题目的求证和求解［5］。但相关的研究成果与本文的研究目标有所不同。前者重在开发计算机的自动推理和自动求解的能力，而本文研究的则是一种比较识别技术，在于识别和判断学生的解答过程与已知的正确解答过程是否等效，而试题中的推演、计算和解答工作仍是由学生自己在计算机上完成，在做题过程中计算机不替代学生做任何工作。国外的相关研究成果与国内大致相同［6-7］。

可以采用任何一个学科都通用的方法对命题逻辑形式推演题目进行评阅。即将学生答案与正确答案进行比较识别，主要利用的是字符串匹配技术，然而由于个人对知识的掌握程度和熟练程度不同可能会使证明步骤数不同，在没有明确要求步骤数的前提下这些也都是正确的，也就造成了一题多解的情况。即使证明的步骤数相同，步骤的顺序不同也会造成多解。这就使评阅过程十分复杂。

命题逻辑中的形式推演仅涉及公式的语法结构，即数理逻辑中命题逻辑的推理证明有严格的程式，它的正确性是能够机械地检验的。可以利用这一特点用计算机实现这类题目的自动评阅。

1 简介

1.1 相关定义

定义1 以“真”、“假”为其变域的变元称为命题变元，命题变元也简称为命题。

定义2 命题演算公式(简称公式)可按以下法则生成［8］:(1)命题是公式;(2)如果P是公式，则┐P是公式;(3)如果 P、Q 是公式，则 P∧Q、P∨Q、P→Q和P↔Q都是公式;⑷只有有限次按照上述法则所得的结果才是公式。

定义3 形式可推演性［9］。A是在命题逻辑中由∑形式可推演(或形式可证明)的，记作∑┠A，当且仅当∑┠A能由(有限次使用)命题逻辑的形式推演规则生成。

定义4 由定义3，∑┠A成立，当且仅当有有限序列:

使得序列(1)中的每一项∑k┠Ak(1≤k≤n)可使用某一形式推演规则生成，并且∑n┠An就是∑┠A(即∑n=∑，An=A)。称序列(1)为形式证明。

1.2 形式推演规则

形式推演将由形式推演的规则定义，在命题逻辑中有以下11条形式推演规则。

这些规则中的每一条都不是单独的一条规则，而是一个规则模式，因为规则中的∑是任何的公式集，A、B和C是任何的公式。

1.3 运算符号的优先级

命题逻辑形式推演中所涉及的运算符号有‘¬’、‘˄’、‘∨’、‘→’、‘↔’，约定每个左方的联结符号优先于右方的联结符号，但“()”可改变优先级，括号内比括号外优先级高，且给定的公式必须符合命题公式所规定的语法规则。

2 评阅系统的建立

2.1 系统总体设计

系统用户包括学生和教师2种。

学生登录后的功能包括在线答题、查询评阅结果、个人信息管理。教师登录后的功能包括评阅试卷，试题管理(增加、修改、删除)，学生管理，个人信息管理。

对于在线实验的样本，首先要解决的问题是如何将复杂的数学公式输入到答题界面。由于本文实验样本是数理逻辑类的推理证明题，只涉及对于→、∈、┐等特殊符号，虽然不能从键盘直接输入到答题界面，但是通过辅助工具帮助学生可以成功完成答题。本文在界面设计时用了一个特殊按钮实现特殊符号的输入。学生在答题时直接通过按钮的Click事件可以轻松完成运算符的编辑，这样的设计适合在线考试系统。本文逻辑证明题实验样本是通过2种方式来完成实验的，在线输入试题并评阅是其中一种方式。另一种方式是学生将答案存成Word文档，再由教师读取到C#建立的评阅界面进行评阅。

实现对学生答案的评阅主要包括以下几个方面:(1)读取学生答案;(2)答案优化;(3)答案处理;(4)答案与形式推演规则模式进行匹配;(5)评分。系统流程图如图1所示。

图1 系统流程图

2.2 答案预处理

2.2.1 试题答案的提取

当考试答题信息以Word样本形式存储在计算机指定位置中时，若要实现计算机的自动评阅首先要解决的问题就是识别Word文档的格式和内容。实际上，在Microsoft Office中集成了VBA(Visual Basic for Application)［10-14］标准宏语言，VBA 提供了访问Word文档的接口，使用 VBA编程可以识别、控制Word 文档的格式［8］。

本文实验是用C#语言编程实现的，C#读取Word文档需要3步完成:(1)对项目添加引用Microsoft Word 11.0 Object Library;(2)在程序集中添加头文件 Using Word=Microsoft.Office.Interop.Word;(3)在指定区域添加打开Word文档所需代码［9］。

2.2.2 答案优化

规范的证明题都要以“证:”或者“证明:”来开始正确解的论证，数理逻辑的证明题也是如此。但是学生答案的核心却是在证明后的证明步骤，所以提取学生答案后首先要做的第一件事情就是剔除不影响答案正误的信息，因此只取“:”后边的正解。利用C#语言中的Split( )实现学生试题中文字信息和试题信息的分离，将取得的关键信息存放在指定数组中，以供后续工作的进行。

2.2.3 答案处理

(1)步骤分离。题目答案由若干步组成，每步为一行，通过将每一行的信息放在相应的Arraylist动态数组中实现步骤分离。

(2)结构分离。用Split函数将每步中的序号、证明内容、证明理由进行分离。

(3)公式分离。证明内容中可能有多个公式，将这些公式分离，并将每步中的条件公式存储在动态数组中，结论公式存储类型为Treenode。Treenode为自定义的二叉树结构类型。

(4)公式表示及判定。每个公式的书写应该符合相应的语法结构，进行准确评分的前提是对公式进行判定。从命题公式的定义可以看出，命题公式的生成过程是一个递归形式，一个命题公式由若干个子公式组成，而子公式又可以包含若干个子公式。由于系统中只有一元和二元的联结词，将命题公式表示成二叉树的形式［15］，树的根节点为命题公式中最后运算的联结词，各子树的根节点对应子公式中最后运算的联结词。叶子节点为公式A，B，C，…。如命题公式A→(A∨B)的二叉树表示形式如图2所示，为了研究的方便，把命题符号和命题联结词符号分别存放在不同的栈中，并记录相应的存放位置。用C#语言［16］形式描述如下:

如果当前字符为运算符，且运算符栈为空，则将字符入栈，否则比较当前运算符和栈顶运算符的优先级，符号栈顶的符号的优先级高于当前符号，将符号栈栈顶符号弹出，并根据该符号是几目符号，将字符栈中的字符弹出，组成子公式，再将子公式压入字符栈，若符号栈顶的符号的优先级低于当前符号，将当前符号压入符号栈。如果是普通字符则将字符直接压入字符栈。字符读取完成之后，从字符栈弹出字符，如果字符栈空则为公式，否则不是公式。

图2 公式A→(A∨B)的二叉树表示形式

2.3 匹配与评分实现

2.3.1 实现算法

(1)将形式证明过程读入系统界面。针对形式证明中的每一步骤，右侧都应写明生成这一步骤所用的证明理由，即所使用的形式推演规则以及所可能涉及的前面已经生成的步骤。

(2)根据证明理由从有关公式的语法结构上检验生成这个步骤时是否正确地使用了形式推演规则。

(3)然后检验形式证明的最后一个步骤是否和所要证明的这个形式可推演性模式相同。如果相同，那么所给出的形式证明就是这个形式可推演性模式的形式证明了，即学生的证明过程正确。

(4)输出框输出检验过程。

2.3.2 核心实现

系统实现最为核心的是11条形式推演规则的代码编写。在1.2节中定义的11条形式推演规则中，(Ref)/(∈)是唯一的直接生成形式可推演模式的规则。使用(+)、(→+)、(˄-)、(∨+)这4 条规则时，要涉及一个已生成的步骤，使用(¬-)、(→-)、(˄+)、(∨-)、(↔-)、(↔+)这6条规则时，要涉及2个已经生成的步骤。将每个规则编写成一个子函数，可以根据每个步骤中所写的理由寻找所使用的推演规则及涉及的步骤调用相应的函数。

形式推演规则仅涉及公式的语法结构。例如使用(→－)，能由:

(1)∑┠A →B

(2)∑┠A生成:

(3)∑┠B

步骤(3)中的前提∑就是步骤(1)和步骤(2)中的前提中的∑，步骤(2)中的结论是步骤(1)中结论的前件，步骤(3)中的结论是步骤(1)中结论的后件。同样可以观察其余的10条规则的情形。因此，只要弄清楚这些规则中公式之间的语法结构上的关系，就能机械地检验是否正确地使用了规则。

3 实验结果及分析

3.1 实例分析

证明:A→(B→C)，(A→B)┠A→C，这是一道数理逻辑中命题逻辑形式推演的证明题，标准答案如下。

证明:

步骤(1)～(3)是根据自反定理得到的，书写顺序是可以颠倒的，如果后边步骤(4)～(7)顺序不变(后边推导条件相应不变)，那么前边步骤有6种书写顺序，这样有6种答案。经过观察可以看出步骤(4)和(5)也是并列关系其顺序也可以颠倒，这样当步骤(4)、(5)颠倒后又有6种答案。对于这些不同的答案该系统都能够正确评阅。

以步骤(4)为例说明每步的评阅过程，读取证明理由“((→ －)，(1)，(2))”，它涉及步骤(1)和(2)，并且使用了推演规则(→-)，判断该步骤正确与否就是要调用推演规则(→－)的函数private Boolean exportdelete(FormDerive one，FormDerive two，Form-Derive three)，看步骤(1)、(2)和(4)的证明内容是否满足(→－)的语法结构(见2.3.2节举例)。对每个步骤都进行上述评阅后，给出最后得分。

3.2 结果分析

本文采用了184个样本进行试验，全部来自于河北工业大学计算机系学生期末考试答题的真实情况，输入成Word文档完成实验。系统能对其中160份样本实现正确的检验，不能100%做出评判的原因有2个:(1)由于样本的书写格式不规范，如没有写推导理由;(2)在证明过程中学生用到11条形式推演规则以外的定理进行证明。可以使用已经证明的形式可推演性模式，因为它们可以归约为规则。所以，形式推演规则是形式推演中的公理，形式可推演性模式是形式推演中的定理。因此，尽管学生的证明过程正确，但是系统不能正确判断。

4 结束语

本文充分利用了C#的强大设计功能和Word对象模型技术，针对命题逻辑形式推演 证明题设计并实现一个自动评分系统。系统具有良好的人机界面和易操作性，并且有效地解决了对于同一个形式推演模式有不同形式证明而给教师带来阅卷困难的问题，大大提高了阅卷效率。

但本系统只适用于形式推演的证明题，有一定的局限性，并且还存在一定的不足(第3.2节中已经指出)，因此系统还需进一步完善。

［1］李学俊.基于人工智能的主观题自动评分算法实现［J］.江南大学学报:自然科学版，2009，8(3):292-295.

［2］吴巧玲.主观题自动评分系统的设计与实现［J］.数字技术与应用，2012(1):113-114.

［3］李兵.初等代数证明题答案的自动检测方法研究［D］.兰州:兰州大学，2012.

［4］杨宁学.作业系统中计算类主观题处理技术研究［D］.成都:西南交通大学，2006.

［5］吴文俊.走向几何的机械化——评Hilbert的名著《几何原理》［J］.数学物理学报，1982(2):125-135.

［6］William H Billingsley.The Intelligent Book:Technologies for Intelligent and Adaptive Textbooks，Focussing on Discrete Mathematics［R］.University of Cambridge，2008.

［7］Ruokokoski J.Automatic Assessment in University-level Mathematics［D］.Helsinki University of Technology，2009.

［8］李刚，杨杰.命题逻辑等值演算的计算机实现［J］.电脑知识与技术:学术交流，2007(2):475-477.

［9］陆钟万.面向计算机科学的数理逻辑(第2版)［M］.北京:科学出版社，2002.

［10］李爱玲，李湘江.基于VBA的Word文档自动评阅技术研究［J］.科学技术与工程，2008，8(17):4859-4863，4868.

［11］Ken Getz，Mike Gilbert.VBA高级开发指南［M］.北京:电子工业出版社，1997.

［12］David Boctor.Microsoft Office 2000 VBA 基础［M］.北京:人民邮电出版社，2000.

［13］申屠浩，鲍可进.用VC++语言创建Word文档［J］.计算机工程与设计，2004，25(6):961-962，967.

［14］陈辉.Word对象模型在智能组卷中的应用［J］.现代电子技术，2012，35(8):39-41，45.

［15］梁晟，赵雷.王浩算法的Java实现［J］.科技信息，2010(5):56，206.

［16］王小科，徐薇.C#从入门到精通［M］.北京:清华大学出版社，2010.