魏 瑋，謝慧珍，張麗純

(河北工業(yè)大學(xué)計(jì)算機(jī)科學(xué)與軟件學(xué)院，天津 300401)

0 引言

面對(duì)越來越多的學(xué)生和高負(fù)荷的閱卷工作，教師要完全細(xì)致地評(píng)閱試卷是件很困難的事。因此計(jì)算機(jī)自動(dòng)閱卷系統(tǒng)的出現(xiàn)有其必然性。對(duì)于客觀題，評(píng)分一般采用簡(jiǎn)單的匹配算法，實(shí)現(xiàn)起來比較容易;而主觀題部分由于操作的多樣性、復(fù)雜性和不確定性使其評(píng)分的實(shí)現(xiàn)難度驟升?，F(xiàn)階段對(duì)主觀題的研究大部分都致力于文字類主觀題［1-2］，對(duì)數(shù)學(xué)類主觀題自動(dòng)評(píng)閱的研究比較少。

國(guó)內(nèi)相關(guān)的研究成果有李兵在其博士論文中實(shí)現(xiàn)了初等代數(shù)證明題答案的自動(dòng)化檢測(cè)［3］和楊寧學(xué)設(shè)計(jì)實(shí)現(xiàn)了基于材料力學(xué)的計(jì)算類主觀題的自動(dòng)評(píng)閱系統(tǒng)［4］。數(shù)理邏輯是數(shù)學(xué)的一個(gè)分支，關(guān)于這方面吳文俊和張景中院士早在幾年前就對(duì)符號(hào)運(yùn)算、公式翻譯和機(jī)器證明技術(shù)進(jìn)行了富有豐碩成果的研究，成功地解決了計(jì)算機(jī)的自動(dòng)推理問題，其重在開發(fā)計(jì)算機(jī)的自動(dòng)推理和自動(dòng)求解的能力，讓計(jì)算機(jī)能夠自動(dòng)完成代數(shù)式的化簡(jiǎn)和恒等變換，或者是幾何題目的求證和求解［5］。但相關(guān)的研究成果與本文的研究目標(biāo)有所不同。前者重在開發(fā)計(jì)算機(jī)的自動(dòng)推理和自動(dòng)求解的能力，而本文研究的則是一種比較識(shí)別技術(shù)，在于識(shí)別和判斷學(xué)生的解答過程與已知的正確解答過程是否等效，而試題中的推演、計(jì)算和解答工作仍是由學(xué)生自己在計(jì)算機(jī)上完成，在做題過程中計(jì)算機(jī)不替代學(xué)生做任何工作。國(guó)外的相關(guān)研究成果與國(guó)內(nèi)大致相同［6-7］。

可以采用任何一個(gè)學(xué)科都通用的方法對(duì)命題邏輯形式推演題目進(jìn)行評(píng)閱。即將學(xué)生答案與正確答案進(jìn)行比較識(shí)別，主要利用的是字符串匹配技術(shù)，然而由于個(gè)人對(duì)知識(shí)的掌握程度和熟練程度不同可能會(huì)使證明步驟數(shù)不同，在沒有明確要求步驟數(shù)的前提下這些也都是正確的，也就造成了一題多解的情況。即使證明的步驟數(shù)相同，步驟的順序不同也會(huì)造成多解。這就使評(píng)閱過程十分復(fù)雜。

命題邏輯中的形式推演僅涉及公式的語法結(jié)構(gòu)，即數(shù)理邏輯中命題邏輯的推理證明有嚴(yán)格的程式，它的正確性是能夠機(jī)械地檢驗(yàn)的?？梢岳眠@一特點(diǎn)用計(jì)算機(jī)實(shí)現(xiàn)這類題目的自動(dòng)評(píng)閱。

1 簡(jiǎn)介

1.1 相關(guān)定義

定義1 以“真”、“假”為其變域的變?cè)Q為命題變?cè)?，命題變?cè)埠?jiǎn)稱為命題。

定義2 命題演算公式(簡(jiǎn)稱公式)可按以下法則生成［8］:(1)命題是公式;(2)如果P是公式，則┐P是公式;(3)如果 P、Q 是公式，則 P∧Q、P∨Q、P→Q和P?Q都是公式;⑷只有有限次按照上述法則所得的結(jié)果才是公式。

定義3 形式可推演性［9］。A是在命題邏輯中由∑形式可推演(或形式可證明)的，記作∑┠A，當(dāng)且僅當(dāng)∑┠A能由(有限次使用)命題邏輯的形式推演規(guī)則生成。

定義4 由定義3，∑┠A成立，當(dāng)且僅當(dāng)有有限序列:

使得序列(1)中的每一項(xiàng)∑k┠Ak(1≤k≤n)可使用某一形式推演規(guī)則生成，并且∑n┠An就是∑┠A(即∑n=∑，An=A)。稱序列(1)為形式證明。

1.2 形式推演規(guī)則

形式推演將由形式推演的規(guī)則定義，在命題邏輯中有以下11條形式推演規(guī)則。

這些規(guī)則中的每一條都不是單獨(dú)的一條規(guī)則，而是一個(gè)規(guī)則模式，因?yàn)橐?guī)則中的∑是任何的公式集，A、B和C是任何的公式。

1.3 運(yùn)算符號(hào)的優(yōu)先級(jí)

命題邏輯形式推演中所涉及的運(yùn)算符號(hào)有‘?’、‘?’、‘∨’、‘→’、‘?’，約定每個(gè)左方的聯(lián)結(jié)符號(hào)優(yōu)先于右方的聯(lián)結(jié)符號(hào)，但“()”可改變優(yōu)先級(jí)，括號(hào)內(nèi)比括號(hào)外優(yōu)先級(jí)高，且給定的公式必須符合命題公式所規(guī)定的語法規(guī)則。

2 評(píng)閱系統(tǒng)的建立

2.1 系統(tǒng)總體設(shè)計(jì)

系統(tǒng)用戶包括學(xué)生和教師2種。

學(xué)生登錄后的功能包括在線答題、查詢?cè)u(píng)閱結(jié)果、個(gè)人信息管理。教師登錄后的功能包括評(píng)閱試卷，試題管理(增加、修改、刪除)，學(xué)生管理，個(gè)人信息管理。

對(duì)于在線實(shí)驗(yàn)的樣本，首先要解決的問題是如何將復(fù)雜的數(shù)學(xué)公式輸入到答題界面。由于本文實(shí)驗(yàn)樣本是數(shù)理邏輯類的推理證明題，只涉及對(duì)于→、∈、┐等特殊符號(hào)，雖然不能從鍵盤直接輸入到答題界面，但是通過輔助工具幫助學(xué)生可以成功完成答題。本文在界面設(shè)計(jì)時(shí)用了一個(gè)特殊按鈕實(shí)現(xiàn)特殊符號(hào)的輸入。學(xué)生在答題時(shí)直接通過按鈕的Click事件可以輕松完成運(yùn)算符的編輯，這樣的設(shè)計(jì)適合在線考試系統(tǒng)。本文邏輯證明題實(shí)驗(yàn)樣本是通過2種方式來完成實(shí)驗(yàn)的，在線輸入試題并評(píng)閱是其中一種方式。另一種方式是學(xué)生將答案存成Word文檔，再由教師讀取到C#建立的評(píng)閱界面進(jìn)行評(píng)閱。

實(shí)現(xiàn)對(duì)學(xué)生答案的評(píng)閱主要包括以下幾個(gè)方面:(1)讀取學(xué)生答案;(2)答案優(yōu)化;(3)答案處理;(4)答案與形式推演規(guī)則模式進(jìn)行匹配;(5)評(píng)分。系統(tǒng)流程圖如圖1所示。

圖1 系統(tǒng)流程圖

2.2 答案預(yù)處理

2.2.1 試題答案的提取

當(dāng)考試答題信息以Word樣本形式存儲(chǔ)在計(jì)算機(jī)指定位置中時(shí)，若要實(shí)現(xiàn)計(jì)算機(jī)的自動(dòng)評(píng)閱首先要解決的問題就是識(shí)別Word文檔的格式和內(nèi)容。實(shí)際上，在Microsoft Office中集成了VBA(Visual Basic for Application)［10-14］標(biāo)準(zhǔn)宏語言，VBA 提供了訪問Word文檔的接口，使用 VBA編程可以識(shí)別、控制Word 文檔的格式［8］。

本文實(shí)驗(yàn)是用C#語言編程實(shí)現(xiàn)的，C#讀取Word文檔需要3步完成:(1)對(duì)項(xiàng)目添加引用Microsoft Word 11.0 Object Library;(2)在程序集中添加頭文件 Using Word=Microsoft.Office.Interop.Word;(3)在指定區(qū)域添加打開Word文檔所需代碼［9］。

2.2.2 答案優(yōu)化

規(guī)范的證明題都要以“證:”或者“證明:”來開始正確解的論證，數(shù)理邏輯的證明題也是如此。但是學(xué)生答案的核心卻是在證明后的證明步驟，所以提取學(xué)生答案后首先要做的第一件事情就是剔除不影響答案正誤的信息，因此只取“:”后邊的正解。利用C#語言中的Split( )實(shí)現(xiàn)學(xué)生試題中文字信息和試題信息的分離，將取得的關(guān)鍵信息存放在指定數(shù)組中，以供后續(xù)工作的進(jìn)行。

2.2.3 答案處理

(1)步驟分離。題目答案由若干步組成，每步為一行，通過將每一行的信息放在相應(yīng)的Arraylist動(dòng)態(tài)數(shù)組中實(shí)現(xiàn)步驟分離。

(2)結(jié)構(gòu)分離。用Split函數(shù)將每步中的序號(hào)、證明內(nèi)容、證明理由進(jìn)行分離。

(3)公式分離。證明內(nèi)容中可能有多個(gè)公式，將這些公式分離，并將每步中的條件公式存儲(chǔ)在動(dòng)態(tài)數(shù)組中，結(jié)論公式存儲(chǔ)類型為Treenode。Treenode為自定義的二叉樹結(jié)構(gòu)類型。

(4)公式表示及判定。每個(gè)公式的書寫應(yīng)該符合相應(yīng)的語法結(jié)構(gòu)，進(jìn)行準(zhǔn)確評(píng)分的前提是對(duì)公式進(jìn)行判定。從命題公式的定義可以看出，命題公式的生成過程是一個(gè)遞歸形式，一個(gè)命題公式由若干個(gè)子公式組成，而子公式又可以包含若干個(gè)子公式。由于系統(tǒng)中只有一元和二元的聯(lián)結(jié)詞，將命題公式表示成二叉樹的形式［15］，樹的根節(jié)點(diǎn)為命題公式中最后運(yùn)算的聯(lián)結(jié)詞，各子樹的根節(jié)點(diǎn)對(duì)應(yīng)子公式中最后運(yùn)算的聯(lián)結(jié)詞。葉子節(jié)點(diǎn)為公式A，B，C，…。如命題公式A→(A∨B)的二叉樹表示形式如圖2所示，為了研究的方便，把命題符號(hào)和命題聯(lián)結(jié)詞符號(hào)分別存放在不同的棧中，并記錄相應(yīng)的存放位置。用C#語言［16］形式描述如下:

如果當(dāng)前字符為運(yùn)算符，且運(yùn)算符棧為空，則將字符入棧，否則比較當(dāng)前運(yùn)算符和棧頂運(yùn)算符的優(yōu)先級(jí)，符號(hào)棧頂?shù)姆?hào)的優(yōu)先級(jí)高于當(dāng)前符號(hào)，將符號(hào)棧棧頂符號(hào)彈出，并根據(jù)該符號(hào)是幾目符號(hào)，將字符棧中的字符彈出，組成子公式，再將子公式壓入字符棧，若符號(hào)棧頂?shù)姆?hào)的優(yōu)先級(jí)低于當(dāng)前符號(hào)，將當(dāng)前符號(hào)壓入符號(hào)棧。如果是普通字符則將字符直接壓入字符棧。字符讀取完成之后，從字符棧彈出字符，如果字符?？談t為公式，否則不是公式。

圖2 公式A→(A∨B)的二叉樹表示形式

2.3 匹配與評(píng)分實(shí)現(xiàn)

2.3.1 實(shí)現(xiàn)算法

(1)將形式證明過程讀入系統(tǒng)界面。針對(duì)形式證明中的每一步驟，右側(cè)都應(yīng)寫明生成這一步驟所用的證明理由，即所使用的形式推演規(guī)則以及所可能涉及的前面已經(jīng)生成的步驟。

(2)根據(jù)證明理由從有關(guān)公式的語法結(jié)構(gòu)上檢驗(yàn)生成這個(gè)步驟時(shí)是否正確地使用了形式推演規(guī)則。

(3)然后檢驗(yàn)形式證明的最后一個(gè)步驟是否和所要證明的這個(gè)形式可推演性模式相同。如果相同，那么所給出的形式證明就是這個(gè)形式可推演性模式的形式證明了，即學(xué)生的證明過程正確。

(4)輸出框輸出檢驗(yàn)過程。

2.3.2 核心實(shí)現(xiàn)

系統(tǒng)實(shí)現(xiàn)最為核心的是11條形式推演規(guī)則的代碼編寫。在1.2節(jié)中定義的11條形式推演規(guī)則中，(Ref)/(∈)是唯一的直接生成形式可推演模式的規(guī)則。使用(+)、(→+)、(?-)、(∨+)這4 條規(guī)則時(shí)，要涉及一個(gè)已生成的步驟，使用(?-)、(→-)、(?+)、(∨-)、(?-)、(?+)這6條規(guī)則時(shí)，要涉及2個(gè)已經(jīng)生成的步驟。將每個(gè)規(guī)則編寫成一個(gè)子函數(shù)，可以根據(jù)每個(gè)步驟中所寫的理由尋找所使用的推演規(guī)則及涉及的步驟調(diào)用相應(yīng)的函數(shù)。

形式推演規(guī)則僅涉及公式的語法結(jié)構(gòu)。例如使用(→－)，能由:

(1)∑┠A →B

(2)∑┠A生成:

(3)∑┠B

步驟(3)中的前提∑就是步驟(1)和步驟(2)中的前提中的∑，步驟(2)中的結(jié)論是步驟(1)中結(jié)論的前件，步驟(3)中的結(jié)論是步驟(1)中結(jié)論的后件。同樣可以觀察其余的10條規(guī)則的情形。因此，只要弄清楚這些規(guī)則中公式之間的語法結(jié)構(gòu)上的關(guān)系，就能機(jī)械地檢驗(yàn)是否正確地使用了規(guī)則。

3 實(shí)驗(yàn)結(jié)果及分析

3.1 實(shí)例分析

證明:A→(B→C)，(A→B)┠A→C，這是一道數(shù)理邏輯中命題邏輯形式推演的證明題，標(biāo)準(zhǔn)答案如下。

證明:

步驟(1)～(3)是根據(jù)自反定理得到的，書寫順序是可以顛倒的，如果后邊步驟(4)～(7)順序不變(后邊推導(dǎo)條件相應(yīng)不變)，那么前邊步驟有6種書寫順序，這樣有6種答案。經(jīng)過觀察可以看出步驟(4)和(5)也是并列關(guān)系其順序也可以顛倒，這樣當(dāng)步驟(4)、(5)顛倒后又有6種答案。對(duì)于這些不同的答案該系統(tǒng)都能夠正確評(píng)閱。

以步驟(4)為例說明每步的評(píng)閱過程，讀取證明理由“((→ －)，(1)，(2))”，它涉及步驟(1)和(2)，并且使用了推演規(guī)則(→-)，判斷該步驟正確與否就是要調(diào)用推演規(guī)則(→－)的函數(shù)private Boolean exportdelete(FormDerive one，F(xiàn)ormDerive two，F(xiàn)orm-Derive three)，看步驟(1)、(2)和(4)的證明內(nèi)容是否滿足(→－)的語法結(jié)構(gòu)(見2.3.2節(jié)舉例)。對(duì)每個(gè)步驟都進(jìn)行上述評(píng)閱后，給出最后得分。

3.2 結(jié)果分析

本文采用了184個(gè)樣本進(jìn)行試驗(yàn)，全部來自于河北工業(yè)大學(xué)計(jì)算機(jī)系學(xué)生期末考試答題的真實(shí)情況，輸入成Word文檔完成實(shí)驗(yàn)。系統(tǒng)能對(duì)其中160份樣本實(shí)現(xiàn)正確的檢驗(yàn)，不能100%做出評(píng)判的原因有2個(gè):(1)由于樣本的書寫格式不規(guī)范，如沒有寫推導(dǎo)理由;(2)在證明過程中學(xué)生用到11條形式推演規(guī)則以外的定理進(jìn)行證明。可以使用已經(jīng)證明的形式可推演性模式，因?yàn)樗鼈兛梢詺w約為規(guī)則。所以，形式推演規(guī)則是形式推演中的公理，形式可推演性模式是形式推演中的定理。因此，盡管學(xué)生的證明過程正確，但是系統(tǒng)不能正確判斷。

4 結(jié)束語

本文充分利用了C#的強(qiáng)大設(shè)計(jì)功能和Word對(duì)象模型技術(shù)，針對(duì)命題邏輯形式推演 證明題設(shè)計(jì)并實(shí)現(xiàn)一個(gè)自動(dòng)評(píng)分系統(tǒng)。系統(tǒng)具有良好的人機(jī)界面和易操作性，并且有效地解決了對(duì)于同一個(gè)形式推演模式有不同形式證明而給教師帶來閱卷困難的問題，大大提高了閱卷效率。

但本系統(tǒng)只適用于形式推演的證明題，有一定的局限性，并且還存在一定的不足(第3.2節(jié)中已經(jīng)指出)，因此系統(tǒng)還需進(jìn)一步完善。

［1］李學(xué)俊.基于人工智能的主觀題自動(dòng)評(píng)分算法實(shí)現(xiàn)［J］.江南大學(xué)學(xué)報(bào):自然科學(xué)版，2009，8(3):292-295.

［2］吳巧玲.主觀題自動(dòng)評(píng)分系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)［J］.數(shù)字技術(shù)與應(yīng)用，2012(1):113-114.

［3］李兵.初等代數(shù)證明題答案的自動(dòng)檢測(cè)方法研究［D］.蘭州:蘭州大學(xué)，2012.

［4］楊寧學(xué).作業(yè)系統(tǒng)中計(jì)算類主觀題處理技術(shù)研究［D］.成都:西南交通大學(xué)，2006.

［5］吳文俊.走向幾何的機(jī)械化——評(píng)Hilbert的名著《幾何原理》［J］.數(shù)學(xué)物理學(xué)報(bào)，1982(2):125-135.

［6］William H Billingsley.The Intelligent Book:Technologies for Intelligent and Adaptive Textbooks，F(xiàn)ocussing 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ì)算機(jī)實(shí)現(xiàn)［J］.電腦知識(shí)與技術(shù):學(xué)術(shù)交流，2007(2):475-477.

［9］陸鐘萬.面向計(jì)算機(jī)科學(xué)的數(shù)理邏輯(第2版)［M］.北京:科學(xué)出版社，2002.

［10］李愛玲，李湘江.基于VBA的Word文檔自動(dòng)評(píng)閱技術(shù)研究［J］.科學(xué)技術(shù)與工程，2008，8(17):4859-4863，4868.

［11］Ken Getz，Mike Gilbert.VBA高級(jí)開發(fā)指南［M］.北京:電子工業(yè)出版社，1997.

［12］David Boctor.Microsoft Office 2000 VBA 基礎(chǔ)［M］.北京:人民郵電出版社，2000.

［13］申屠浩，鮑可進(jìn).用VC++語言創(chuàng)建Word文檔［J］.計(jì)算機(jī)工程與設(shè)計(jì)，2004，25(6):961-962，967.

［14］陳輝.Word對(duì)象模型在智能組卷中的應(yīng)用［J］.現(xiàn)代電子技術(shù)，2012，35(8):39-41，45.

［15］梁晟，趙雷.王浩算法的Java實(shí)現(xiàn)［J］.科技信息，2010(5):56，206.

［16］王小科，徐薇.C#從入門到精通［M］.北京:清華大學(xué)出版社，2010.