王湘云

(華北水利水電大學(xué)，鄭州 450011)

邏輯教學(xué)軟件及其實(shí)效性研究

王湘云

(華北水利水電大學(xué)，鄭州 450011)

作為現(xiàn)代化教育技術(shù)的一個(gè)重要手段，邏輯教學(xué)軟件在邏輯教育過(guò)程中發(fā)揮著十分重要的作用。邏輯教學(xué)軟件的使用可以提高教學(xué)質(zhì)量和教學(xué)效率，促進(jìn)邏輯教學(xué)現(xiàn)代化的發(fā)展，也有利于學(xué)生更好地理解邏輯的思想，更有效地掌握邏輯的方法。為此，介紹一些國(guó)際上流行的邏輯教學(xué)軟件，以及國(guó)內(nèi)邏輯教學(xué)中邏輯軟件的使用情況，并討論邏輯教學(xué)軟件的實(shí)效性。

邏輯教學(xué)軟件;教育技術(shù)現(xiàn)代化;邏輯教學(xué)現(xiàn)代化;實(shí)效性

20世紀(jì)90年代以來(lái)，一批具有新時(shí)代特色的邏輯學(xué)教材應(yīng)運(yùn)而生，邏輯教學(xué)探索與改革成果豐碩。隨著現(xiàn)代數(shù)字和信息技術(shù)的飛速發(fā)展，在邏輯教學(xué)中運(yùn)用新媒體和現(xiàn)代教育技術(shù)的手段也日趨成熟。這些實(shí)踐促進(jìn)了邏輯學(xué)的教學(xué)改革，提升了邏輯學(xué)的教學(xué)水平，也增強(qiáng)了邏輯學(xué)的教學(xué)效果。

作為現(xiàn)代化教育技術(shù)的一個(gè)重要手段，邏輯教學(xué)軟件在邏輯教育過(guò)程中的作用越來(lái)越顯著。邏輯教學(xué)軟件的使用，有利于學(xué)生更好地理解邏輯的思想，更有效地掌握邏輯的方法［1］，給高校邏輯學(xué)教育帶來(lái)了新的機(jī)遇和挑戰(zhàn)。

一、邏輯教學(xué)軟件產(chǎn)生的背景

邏輯學(xué)和計(jì)算機(jī)的關(guān)系非常密切，特別是現(xiàn)代邏輯的研究方法和研究成果在計(jì)算機(jī)科學(xué)各領(lǐng)域都有廣泛的應(yīng)用。

12世紀(jì)末13世紀(jì)初，西班牙邏輯學(xué)家羅門·盧樂(lè)(Romen Luee)提出了制造可解決各種問(wèn)題的通用邏輯機(jī)，初步揭示了人類思維與計(jì)算可同一的思想。17世紀(jì)，德國(guó)數(shù)學(xué)家和哲學(xué)家萊布尼茲(G．W．Leibniz)改進(jìn)了帕斯卡(B．Pascal)的加法數(shù)字計(jì)算器，做出了四則運(yùn)算的手搖計(jì)算器，并提出了“通用符號(hào)”和“推理計(jì)算”的思想，使形式邏輯符號(hào)化，這可以說(shuō)是“機(jī)器思維”研究的萌芽。19世紀(jì)，英國(guó)數(shù)學(xué)家布爾(G．Boole)創(chuàng)立了布爾代數(shù)，第一次用符號(hào)語(yǔ)言描述了思維的基本推理法則，真正使邏輯代數(shù)化。布爾系統(tǒng)奠定了現(xiàn)代形式邏輯研究的基礎(chǔ)。20世紀(jì)初期，懷特海(A．N．Whitehead)和羅素(B．A．W．Russel)在合著的《數(shù)學(xué)原理》(1910-1913)中，提出了從純形式系統(tǒng)的角度(即機(jī)械角度)來(lái)處理數(shù)學(xué)推理的方法，為數(shù)學(xué)推理在計(jì)算機(jī)上的自動(dòng)化實(shí)現(xiàn)奠定了理論基礎(chǔ)。他們開(kāi)發(fā)的邏輯句法和形式推理規(guī)則是自動(dòng)定理證明系統(tǒng)的基礎(chǔ)，也是人工智能的理論基礎(chǔ)。

1937年，英國(guó)數(shù)學(xué)家圖靈(A．M．Turing)建立了描述算法的機(jī)械性思維過(guò)程，提出了理想計(jì)算機(jī)模型(即圖靈機(jī))，創(chuàng)立了自動(dòng)機(jī)理論，奠定了整個(gè)計(jì)算機(jī)科學(xué)的理論基礎(chǔ)。據(jù)此，1945年匈牙利數(shù)學(xué)家馮·諾依曼(John Von Neumann)提出了存儲(chǔ)程序的思想，并建立了通用電子數(shù)字計(jì)算機(jī)的馮·諾依曼型體系結(jié)構(gòu);1946年美國(guó)的莫克利(J．W．Mauchly)和埃克特(J．P．Eckert)成功研制出世界上第一臺(tái)通用電子數(shù)學(xué)計(jì)算機(jī)ENIAC［2］。

20世紀(jì)中期，人們開(kāi)始設(shè)想用計(jì)算機(jī)進(jìn)行邏輯推理。1956年，國(guó)際著名的邏輯學(xué)家、數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家紐厄爾(A．Newell)和西蒙(H．A．Simon)等人首先取得突破，他們編制的模擬人的啟發(fā)式搜索問(wèn)題解決的計(jì)算機(jī)程序“邏輯理論家”證明了羅素和懷德海合著的《數(shù)學(xué)原理》第二章中的38條邏輯推理。后來(lái)經(jīng)過(guò)改進(jìn)，又證明了該章的全部52條邏輯推理。此后，世界著名邏輯學(xué)家美籍華人王浩教授在IBM-704計(jì)算機(jī)上以3～5分鐘的時(shí)間證明了《數(shù)學(xué)原理》中有關(guān)命題演算的全部220條邏輯推理，并且還證明了該書(shū)中帶等詞的謂詞演算的150條邏輯推理的85%。不久，他僅用8．4分鐘的時(shí)間證明了以上全部邏輯推理［3］。同一時(shí)期，我國(guó)著名數(shù)學(xué)家吳文俊教授也在自動(dòng)定理證明方面做出了突出的貢獻(xiàn)，他提出的把幾何問(wèn)題代數(shù)化的方法被國(guó)際上的學(xué)者稱為“吳方法”。隨著計(jì)算機(jī)科學(xué)技術(shù)的迅速發(fā)展，自動(dòng)推理的作用顯得越來(lái)越重要，許多邏輯學(xué)家嘗試使用計(jì)算機(jī)來(lái)模擬邏輯的思想和方法，從而研發(fā)了一系列的邏輯軟件，推動(dòng)了邏輯學(xué)教育技術(shù)的現(xiàn)代化?，F(xiàn)代信息技術(shù)帶來(lái)了現(xiàn)代化的教學(xué)手段，也對(duì)傳統(tǒng)的教學(xué)方式和教學(xué)手段進(jìn)行了革新。同多媒體課件、電子學(xué)習(xí)資源、網(wǎng)絡(luò)課程等現(xiàn)代化的教育技術(shù)手段一樣，邏輯教學(xué)軟件在邏輯教學(xué)過(guò)程也發(fā)揮著十分重要的作用。

進(jìn)入21世紀(jì)，邏輯軟件的開(kāi)發(fā)及在邏輯教學(xué)中的應(yīng)用逐漸成為邏輯教育過(guò)程中極為重要的一個(gè)環(huán)節(jié)。2000年、2006年和2011年，在西班牙的薩拉曼卡大學(xué)，分別召開(kāi)了3次關(guān)于“邏輯教學(xué)工具”的國(guó)際性學(xué)術(shù)研討會(huì)。這3次會(huì)議將邏輯教學(xué)軟件的開(kāi)發(fā)和使用作為重要議題來(lái)討論，對(duì)邏輯軟件的發(fā)展前景、邏輯教學(xué)軟件在邏輯教學(xué)中的作用等具體問(wèn)題進(jìn)行了深入的研究，引起了邏輯學(xué)界對(duì)邏輯教學(xué)軟件的廣泛興趣和重視，有力地推動(dòng)了邏輯教學(xué)軟件的發(fā)展。

二、邏輯教學(xué)軟件的研究狀況

從操作模式來(lái)看，邏輯軟件主要有計(jì)算機(jī)網(wǎng)絡(luò)在線邏輯軟件和計(jì)算機(jī)程序設(shè)計(jì)邏輯軟件兩類。計(jì)算機(jī)網(wǎng)絡(luò)在線邏輯軟件是基于萬(wàn)維網(wǎng)的，有邏輯教學(xué)網(wǎng)絡(luò)平臺(tái)的支持，并由軟件供應(yīng)商提供程序在線服務(wù)。在線邏輯軟件有對(duì)應(yīng)的網(wǎng)絡(luò)鏈接，學(xué)習(xí)者直接在網(wǎng)絡(luò)界面下使用，可以進(jìn)行互動(dòng)練習(xí)，操作簡(jiǎn)便。計(jì)算機(jī)程序設(shè)計(jì)邏輯軟件是用某種程序設(shè)計(jì)語(yǔ)言編寫，運(yùn)行于Windows或Mac等操作系統(tǒng)上的應(yīng)用軟件。程序設(shè)計(jì)邏輯軟件由用戶安裝在計(jì)算機(jī)中，執(zhí)行特定的功能，操作具有獨(dú)立性。根據(jù)形式邏輯的分類，邏輯軟件也可分為傳統(tǒng)邏輯軟件、數(shù)理邏輯軟件、哲學(xué)邏輯軟件等等。

(一)國(guó)外邏輯教學(xué)軟件的研究

國(guó)外對(duì)邏輯軟件的研發(fā)已經(jīng)取得了豐富的成果。早在1980年，美國(guó)斯坦福大學(xué)語(yǔ)言與信息研究中心(CSLI)就研發(fā)了一系列具有開(kāi)創(chuàng)性和實(shí)效性的邏輯應(yīng)用軟件，用于本科生數(shù)理邏輯課程的教學(xué)和研究。目前，在國(guó)外的大學(xué)邏輯學(xué)教學(xué)中，較多地使用了邏輯軟件，特別是一些現(xiàn)代邏輯軟件的應(yīng)用已經(jīng)相當(dāng)?shù)爻墒旌屯晟啤?/p>

我們參考國(guó)外的邏輯教育網(wǎng)站，簡(jiǎn)要介紹一些流行且實(shí)用的邏輯軟件。

1．亞里士多德詞項(xiàng)邏輯(Computational Aristotelian Term Logic)①網(wǎng)址:http://logic．glashoff．net/aristotelianlogic/

亞里士多德詞項(xiàng)邏輯是由德國(guó)邏輯學(xué)家克勞斯·格拉斯霍夫(Klaus Glashoff)于2004年開(kāi)發(fā)的一款傳統(tǒng)邏輯軟件。這款邏輯在線軟件的主要功能是學(xué)習(xí)亞里士多德三段論邏輯的自然演繹系統(tǒng)。該軟件預(yù)設(shè)了全部的三段論演繹規(guī)則，輸入三段論的前提，并選擇相應(yīng)的有效論式，執(zhí)行后就可以直接得到結(jié)論。

2．邏輯工具箱(Logic Toolbox)②網(wǎng)址:http://philosophy．lander．edu/～jsaetti/ToolBox/dojoCateg/categorical．html

邏輯工具箱是約翰·薩埃蒂(John Saetti)于2009年開(kāi)發(fā)的一個(gè)在線教學(xué)平臺(tái)。其中的范疇邏輯計(jì)算器(Categorical Logic)也是一款關(guān)于三段論學(xué)習(xí)的傳統(tǒng)邏輯軟件。該軟件對(duì)傳統(tǒng)邏輯性質(zhì)判斷中的主項(xiàng)和謂項(xiàng)之間的外延關(guān)系，用構(gòu)造出的文恩圖做出判斷和檢驗(yàn)，還可以進(jìn)行直言推理、三段論推理、連鎖推理和省略式三段論推理。

3．樹(shù)證明發(fā)生器(Tree Proof Generater)③網(wǎng)址:http://www．umsu．de/logik/trees/

樹(shù)證明發(fā)生器是由沃爾夫?qū)?Wolfgang Schwarz)于2007年11月發(fā)布的一個(gè)利用JavaS-cript程序設(shè)計(jì)的在線邏輯軟件。樹(shù)證明的方法也稱作語(yǔ)義表，是檢查各種邏輯公式有效性的一種有效算法。這款數(shù)理邏輯軟件為經(jīng)典的命題邏輯和不含等詞的謂詞邏輯提供語(yǔ)義表。用戶只需輸入要驗(yàn)證的、有效的命題公式或謂詞公式，系統(tǒng)就會(huì)自動(dòng)生成一棵證明樹(shù)或者給出反模型的證明。

4．邏輯動(dòng)畫入門(Introductory Logic Animations)④網(wǎng)址:http://staff．science．uva．nl/～jaspars/animations/

1988—1999年，由荷蘭阿姆斯特丹大學(xué)的賈恩(Jan Jaspars)等人開(kāi)發(fā)的邏輯動(dòng)畫入門也是利用JavaScript程序設(shè)計(jì)的一個(gè)在線邏輯軟件。該軟件可以對(duì)基礎(chǔ)數(shù)理邏輯和哲學(xué)邏輯的形式演算進(jìn)行互動(dòng)訓(xùn)練，包括命題邏輯、謂詞邏輯、模態(tài)邏輯、動(dòng)態(tài)邏輯和圖靈機(jī)5個(gè)功能模塊，每一個(gè)功能模塊又由若干子程序組成。例如，命題邏輯功能模塊下的子程序:命題計(jì)算器(propositional calculator)可判定一個(gè)命題邏輯公式是否是重言式、矛盾式或可滿足式，以及該公式真值為真或假時(shí)，其命題變項(xiàng)的真值組合。謂詞邏輯功能模塊下的子程序:謂詞計(jì)算器(predicate calculator)用來(lái)計(jì)算給定模型上的謂詞邏輯公式的結(jié)果，并查找自由變項(xiàng)的正反實(shí)例。模態(tài)邏輯功能模塊的子程序:可能世界計(jì)算器(possible world calculator)可在一個(gè)給定的克里普克(Kripke)模型中計(jì)算出哪些世界能夠驗(yàn)證輸入的模態(tài)公式。動(dòng)態(tài)邏輯功能模塊下的子程序:傳遞計(jì)算器(transition calculator)可以計(jì)算一個(gè)給定正則表達(dá)式的傳遞外延。

5．交互式邏輯程序(Interactive Logic Programs)⑤網(wǎng)址:http://www．math．uwaterloo．ca/～snburris/htdocs/LOGIC/st-ilp．html

交互式邏輯程序是加拿大滑鐵盧大學(xué)的斯坦利·貝爾雷斯(Stanley N．Burris)開(kāi)發(fā)的在線教學(xué)平臺(tái)，包括真值表(Truth Tables)、命題聯(lián)結(jié)詞(Propositional Connectives)、戴維斯-帕特南程序(Davis-Putnam procedure)、合一算法(Unification A lgorithm)、自動(dòng)定理證明器(Automated Theorem Prover)等一系列邏輯軟件。例如，命題聯(lián)結(jié)詞程序可令用戶選擇任意的常項(xiàng)0、1，否定詞“﹁”和16進(jìn)制的二元聯(lián)結(jié)詞，然后驗(yàn)證哪些聯(lián)結(jié)詞可以由已選定的聯(lián)結(jié)詞得到。戴維斯-帕特南程序允許用戶最多選擇10個(gè)子句，然后后臺(tái)運(yùn)用戴維斯-帕特南方法確定所選子句集是否是可滿足的。合一算法程序允許用戶選擇兩個(gè)前綴形式的項(xiàng)，然后找出它們的一致置換，等等。

6．柏拉圖(Plato)⑥網(wǎng)址:http://www．utexas．edu/courses/plato/index．html

柏拉圖是美國(guó)得克薩斯大學(xué)的羅伯特·昆斯(Robert C．Koons)開(kāi)發(fā)的邏輯在線教學(xué)平臺(tái)，用于形式邏輯基礎(chǔ)課程的學(xué)習(xí)，內(nèi)容包括在線課程、軟件下載、學(xué)習(xí)指南、專業(yè)詞典等。柏拉圖程序能夠使用戶構(gòu)造命題演算和謂詞演算形式語(yǔ)言中的證明，也可用來(lái)構(gòu)造包括集合論部分在內(nèi)的形式化的數(shù)學(xué)證明。

7．通向邏輯之門(Gateway to Logic)⑦網(wǎng)址:http://logik．phl．univie．a(chǎn)c．a(chǎn)t/～chris/gateway/formularuk．htm l

奧地利維也納大學(xué)的克里斯汀·戈特沙爾(Christian Gottschall)開(kāi)發(fā)的通向邏輯之門在線平臺(tái)集一些基于網(wǎng)絡(luò)的邏輯程序?yàn)橐惑w，并提供了一些邏輯函數(shù)，如真值表、范式、證明檢驗(yàn)、證明構(gòu)造等。服務(wù)器端函數(shù)(Server-side Functions)用來(lái)計(jì)算經(jīng)典二值命題邏輯的公式，由真值表、重言式檢驗(yàn)、圖解表達(dá)式樹(shù)、文本表達(dá)式樹(shù)、合取范式、典范合取范式、析取范式、典范析取范式等一系列函數(shù)組成。證明生成器(Proof Builder)是能夠交互式地構(gòu)造證明的程序。證明檢查器(Proof Checker)可以檢驗(yàn)用戶提交的證明。自動(dòng)定理證明器(Automated Theorem Prover)適用于經(jīng)典的謂詞邏輯，可以自動(dòng)地推出有效論證，直接在服務(wù)器端上執(zhí)行。

8．阿卡網(wǎng)絡(luò)平臺(tái)(Akka flies the Web)①網(wǎng)址:http://staff．science．uva．nl/～lhendrik/AkkaStart．html

荷蘭阿姆斯特丹大學(xué)的萊克斯(Lex Hendriks)于1998年開(kāi)發(fā)的阿卡網(wǎng)絡(luò)平臺(tái)可以檢驗(yàn)一些邏輯系統(tǒng)中公式的可證明性和模型中公式的有效性，為動(dòng)態(tài)邏輯繪制并編輯克里普克模型，以及用計(jì)算機(jī)測(cè)定邏輯語(yǔ)義圖。阿卡是對(duì)克里普克模型進(jìn)行定理測(cè)試和模型測(cè)試的工具，提供克里普克模型編輯器并且支持模型測(cè)試，還可提供附加的服務(wù)，如語(yǔ)義圖的構(gòu)造。

此外，瑞士伯爾尼大學(xué)開(kāi)發(fā)的邏輯工作臺(tái)(The LogicsWorkbench)，②網(wǎng)址:http://www．lwb．unibe．ch/美國(guó)德克薩斯州農(nóng)業(yè)機(jī)械大學(xué)開(kāi)發(fā)的邏輯后臺(tái)程序和課堂測(cè)驗(yàn)(Logic Daemon and Quizmaster)，③網(wǎng)址:http://logic．tamu．edu/美國(guó)猶他大學(xué)開(kāi)發(fā)的表達(dá)式計(jì)算器(Expression Evaluator)④網(wǎng)址:http://www．cc．utah．edu/～nahaj/logic/evaluate/等等，都是用于形式邏輯學(xué)習(xí)的在線邏輯教學(xué)平臺(tái)。

9．語(yǔ)言、證明和邏輯(Language，Proof and Logic)

語(yǔ)言、證明和邏輯教學(xué)軟件包，簡(jiǎn)稱LPL，是美國(guó)斯坦福大學(xué)語(yǔ)言與信息研究中心(CSLI)研發(fā)的一套專門用于一階邏輯語(yǔ)言學(xué)習(xí)的計(jì)算機(jī)程序組件。該教學(xué)軟件包與美國(guó)邏輯學(xué)家、印第安那大學(xué)的巴威斯(Jon Barwise)及其在斯坦福大學(xué)語(yǔ)言與信息研究中心的同事艾克曼迪(John Etchemendy)合著的《一階邏輯的語(yǔ)言》，以及他們二人合著的改進(jìn)版本《語(yǔ)言、證明和邏輯》二書(shū)配套使用［4］。LPL軟件包是目前最為成熟、功能上更加完善的一組數(shù)理邏輯學(xué)習(xí)軟件，包括布爾(Boole)、費(fèi)奇(Fitch)、塔斯基的世界(Tarski’s World)3個(gè)邏輯程序和一個(gè)基于互聯(lián)網(wǎng)的分等級(jí)服務(wù):提交(Subm it)。這些程序能在計(jì)算機(jī)操作系統(tǒng)Windows或Mac下使用。

布爾程序用于構(gòu)造邏輯公式的真值表。其最大的特點(diǎn)就是對(duì)公式中所含命題變項(xiàng)的個(gè)數(shù)沒(méi)有限制并能同時(shí)構(gòu)造若干個(gè)命題的真值表。塔斯基的世界程序用于學(xué)習(xí)一階語(yǔ)言及其語(yǔ)義。用戶可以在該程序設(shè)計(jì)的三維空間里使用和改造已有的世界或創(chuàng)造新的世界，編寫一階邏輯的語(yǔ)句，判斷它們的真值，還可以通過(guò)做游戲，檢驗(yàn)自己對(duì)語(yǔ)句真值的判斷是否正確，從而掌握邏輯聯(lián)結(jié)詞和量詞的用法。費(fèi)奇程序用于構(gòu)造自然推理系統(tǒng)F下的形式證明。用戶可以運(yùn)用相應(yīng)的推理規(guī)則分步驟驗(yàn)證一階公式的形式證明。提交程序用于網(wǎng)上提交作業(yè)。學(xué)生的作業(yè)可以直接遞交給評(píng)分服務(wù)器(Grade Grinder)，它將給作業(yè)評(píng)分并將結(jié)果發(fā)送給學(xué)生及導(dǎo)師。

10．超證明(Hyperproof)

超證明也是由巴威斯和艾克曼迪共同研發(fā)的一款用于分析謂詞邏輯自然演繹形式的推理過(guò)程的程序軟件。這款程序僅適用于蘋果機(jī)型，與二人1994出版的《超證明》一書(shū)配套使用。

超證明是分析推論和證明過(guò)程的規(guī)則的一個(gè)學(xué)習(xí)系統(tǒng)，與傳統(tǒng)的對(duì)一階邏輯處理的方式不同，它包含圖形信息和句子信息，綜合不同的信息形式，描述出一系列的推理規(guī)則。這種方式能夠使學(xué)生集中于證明內(nèi)容的信息，而不是句子的語(yǔ)法結(jié)構(gòu)，從而利用一種直觀的證明系統(tǒng)，學(xué)會(huì)構(gòu)建后承和非后承的證明，將標(biāo)準(zhǔn)的句法規(guī)則擴(kuò)展為用圖形表示的合并信息。超證明軟件能夠檢查每一證明類型的邏輯有效性，適用于各種自然演繹形式的證明系統(tǒng)，包括巴威斯和艾克曼迪的一階邏輯語(yǔ)言的系統(tǒng)。還適用于塔斯基的世界程序，能構(gòu)造和檢查塔斯基的世界語(yǔ)言中的證明。它允許用戶將圖形表示的信息和圖形相適合的演繹技術(shù)、句子和語(yǔ)法規(guī)則組合，對(duì)塔斯基的世界中的塊世界進(jìn)行推理，使得學(xué)習(xí)一階邏輯具有極大的樂(lè)趣。

11．超求解器(Hypersolver)

超求解器是由土爾其比爾肯大學(xué)的阿克曼(V．Akman)和土爾其海峽大學(xué)的帕克坎(M．Pakkan)于1993年研發(fā)的一款利用解引理在非良基集合全域中解方程的程序軟件。非良基集合(Non-well-founded sets)，也稱超集(Hypersets)，是具有循環(huán)性質(zhì)或無(wú)窮∈降鏈性質(zhì)的集合。1987年，美國(guó)著名邏輯學(xué)家巴威斯(J．Barwise)和艾切曼迪(J．Etchemendy)為了證明非良基集合的存在性，引入解引理說(shuō)明每個(gè)方程組有唯一解，即把集合看作方程組的解。為了得到更為豐富的集合全域，保證非良基集合的存在，以便對(duì)各種循環(huán)現(xiàn)象做出解釋，可以在標(biāo)準(zhǔn)集合論中用非良基公理替換良基公理，從而得到非良基集合論。而非良基集合論給出了一套完備的工具能夠刻畫現(xiàn)實(shí)世界中各種各樣的循環(huán)問(wèn)題。就此而言，非良基集合論的作用和影響已經(jīng)遠(yuǎn)遠(yuǎn)超出了經(jīng)典的集合論ZFC［5］。

解引理是非良基集合論的特色。超求解程序，是一個(gè)基于解引理的、獨(dú)立操作的程序，可以對(duì)根據(jù)集合定義的方程組進(jìn)行求解。它具有內(nèi)置的圖解功能，能夠顯示出描述用戶輸入方程以及這些方程解的圖。超求解器的用戶接口，稱作命令接口。用戶輸入有效的一個(gè)文件，文件中的每一行都是一個(gè)方程，文件被送到語(yǔ)法解析器轉(zhuǎn)變?yōu)長(zhǎng)isp(列表處理語(yǔ)言)形式，并檢驗(yàn)是否符合輸入要求。之后，超求解器的解算器將解引理應(yīng)用到所輸入的方程組，進(jìn)行求解。接下來(lái)是圖顯示部件的調(diào)用，這一部件輸入解算器產(chǎn)生的方程組的解，最后由圖繪制程序描述出方程組的解決方案圖并顯示在圖顯示窗中。

除了具有數(shù)學(xué)上的重要性和精確性之外，超求解器還提供了刻畫各種循環(huán)現(xiàn)象的一種有趣的方法。在人工智能領(lǐng)域中，信息能夠以方程組的形式來(lái)安排，因而該程序是進(jìn)行常識(shí)推理的一個(gè)非常有用的實(shí)用工具。超求解程序具有一般的語(yǔ)法分析器和直觀的圖形界面，也是數(shù)理邏輯的重要工具程序之一。超求解程序的實(shí)施，使得利用解引理模型化循環(huán)的現(xiàn)象同計(jì)算機(jī)自動(dòng)化求解問(wèn)題緊密地結(jié)合起來(lái)，極具應(yīng)用價(jià)值［6］。

(二)國(guó)內(nèi)邏輯教學(xué)軟件的研究

國(guó)內(nèi)對(duì)邏輯教學(xué)軟件的研究相對(duì)國(guó)外而言還十分薄弱，剛剛進(jìn)入起步階段。2007年5月，南開(kāi)大學(xué)哲學(xué)院建設(shè)了國(guó)內(nèi)第一個(gè)“邏輯推理”實(shí)驗(yàn)室，也是目前國(guó)內(nèi)高校中唯一的一個(gè)用于邏輯學(xué)學(xué)科教學(xué)的實(shí)驗(yàn)平臺(tái)。該實(shí)驗(yàn)室具有多媒體網(wǎng)絡(luò)功能，配備有蘋果iMac、激光打印機(jī)、投影機(jī)等硬件設(shè)備和LPL、超證明等一些邏輯教學(xué)軟件，主要用于邏輯學(xué)專業(yè)本科生和研究生數(shù)理邏輯課程的實(shí)驗(yàn)教學(xué)。實(shí)驗(yàn)室的建立，改善了邏輯學(xué)學(xué)科的教學(xué)條件，在該學(xué)科領(lǐng)域的教學(xué)中引入現(xiàn)代化技術(shù)，逐漸與國(guó)際邏輯學(xué)教學(xué)接軌。

近幾年來(lái)，實(shí)驗(yàn)室負(fù)責(zé)人李娜教授及成員在數(shù)理邏輯課程的教學(xué)過(guò)程中，將邏輯軟件同邏輯學(xué)教科書(shū)、教學(xué)課件一樣作為教學(xué)工具來(lái)使用。實(shí)驗(yàn)室使用的邏輯軟件主要是從國(guó)外購(gòu)買的教學(xué)軟件包，以及國(guó)外的網(wǎng)絡(luò)在線教學(xué)軟件。此外，實(shí)驗(yàn)室還開(kāi)發(fā)了兩個(gè)教學(xué)軟件，一個(gè)是能夠快速構(gòu)造真值表、計(jì)算命題公式真值的邏輯軟件:邏輯運(yùn)算3．0。①網(wǎng)址:http://phil．nankai．edu．cn/sllg/index．htm這款軟件有中英兩個(gè)版本，適用于Windows操作平臺(tái)，能夠計(jì)算不超過(guò)6個(gè)命題變項(xiàng)的命題公式的真值，并能列出不超過(guò)6個(gè)命題變項(xiàng)的命題公式的真值表。另一個(gè)是數(shù)理邏輯學(xué)習(xí)詞典。雖然這兩個(gè)軟件的功能相對(duì)簡(jiǎn)單且還不夠完善，但總算打破了國(guó)內(nèi)邏輯學(xué)軟件的研發(fā)一直是空白的境況。

李娜教授編寫出版了兩本邏輯實(shí)驗(yàn)教材:《數(shù)理邏輯實(shí)驗(yàn)教程》和《邏輯學(xué)實(shí)驗(yàn)教程》。前者主要針對(duì)數(shù)理邏輯的學(xué)習(xí)及數(shù)理邏輯軟件的使用，后者是包括亞里士多德三段論邏輯、數(shù)理邏輯和哲學(xué)邏輯(模態(tài)邏輯)的完全形式化推理的實(shí)驗(yàn)教材。

目前，實(shí)驗(yàn)室還在繼續(xù)建設(shè)當(dāng)中，實(shí)驗(yàn)室與臺(tái)灣東吳大學(xué)的林正弘教授就國(guó)際上一些邏輯教學(xué)軟件的使用情況進(jìn)行了交流;2008年10月，世界邏輯學(xué)家本特姆(Johan van Benthem)先生到實(shí)驗(yàn)室參觀和交流，并對(duì)邏輯動(dòng)畫入門軟件中的更新和驗(yàn)算器進(jìn)行了深入的講解;2011年10月7日，南開(kāi)大學(xué)哲學(xué)院召開(kāi)了“邏輯學(xué)開(kāi)放教學(xué)與網(wǎng)絡(luò)應(yīng)用軟件”國(guó)際研討會(huì)，來(lái)自美國(guó)斯坦福大學(xué)、荷蘭阿姆斯特丹大學(xué)、西班牙塞維利亞大學(xué)、印度晨奈數(shù)學(xué)研究所、新西蘭奧克蘭大學(xué)，以及清華大學(xué)、北京大學(xué)、浙江大學(xué)、中山大學(xué)、南開(kāi)大學(xué)的學(xué)者就邏輯教學(xué)使用的工具和方法等內(nèi)容進(jìn)行了探討;實(shí)驗(yàn)室也得到了艾切曼迪先生、清華大學(xué)劉奮榮教授以及其他邏輯學(xué)界專家的很多幫助。

回顧國(guó)內(nèi)外邏輯教學(xué)軟件的研究成果，國(guó)內(nèi)與國(guó)外的差距顯著。國(guó)外邏輯教學(xué)軟件的開(kāi)發(fā)和研究己經(jīng)蓬勃興起，內(nèi)容涵蓋廣泛，涉及傳統(tǒng)邏輯、數(shù)理邏輯、哲學(xué)邏輯以及其他更深層次的現(xiàn)代邏輯分支。阿姆斯特丹大學(xué)、斯坦福大學(xué)、哈佛學(xué)院、哥倫比亞大學(xué)等國(guó)際知名學(xué)校在邏輯學(xué)教學(xué)中都已采用了相應(yīng)的邏輯教學(xué)軟件，并取得了顯著的效果。

三、邏輯教學(xué)軟件的實(shí)效性

邏輯教學(xué)軟件的實(shí)效性是指在高等院校邏輯學(xué)教育過(guò)程中，使用邏輯教學(xué)軟件這種現(xiàn)代化教育技術(shù)手段的實(shí)際結(jié)果或客觀效果。通常表現(xiàn)為邏輯教學(xué)軟件對(duì)大學(xué)生的影響程度或大學(xué)生接受使用邏輯教學(xué)軟件的邏輯學(xué)教育后的實(shí)際效果。新時(shí)期下，邏輯教學(xué)軟件正以其獨(dú)有的優(yōu)勢(shì)逐步深入到邏輯學(xué)教學(xué)中。邏輯教學(xué)軟件的實(shí)效性主要體現(xiàn)在以下幾個(gè)方面。

(一)提高教學(xué)質(zhì)量和教學(xué)效率

盡管邏輯學(xué)理論的研究取得了顯著的成果，但邏輯學(xué)教學(xué)的狀況并不樂(lè)觀，特別是在我國(guó)高等教育中。近幾年來(lái)，邏輯通識(shí)教育面臨各種困境，有關(guān)邏輯學(xué)教學(xué)方面的研究成果很少。邏輯教學(xué)軟件的產(chǎn)生和發(fā)展及其在課堂教學(xué)中的逐漸應(yīng)用，促使了邏輯教學(xué)水平的不斷提高。邏輯學(xué)較其他基礎(chǔ)課而言，難學(xué)、難懂、難掌握，尤其是現(xiàn)代邏輯的內(nèi)容更加抽象。基于網(wǎng)絡(luò)和計(jì)算機(jī)平臺(tái)的邏輯軟件具有可視化的界面，形象、直觀、生動(dòng)、具體，而且內(nèi)容豐富，可以容納大量教學(xué)材料或?qū)嵗?。許多繁瑣的、重復(fù)的、形式化的推理演算和驗(yàn)證工作，甚至教師需要評(píng)分的習(xí)題，都可以交給邏輯軟件來(lái)完成，既節(jié)省時(shí)間，又減少錯(cuò)誤，能夠有效地提高教學(xué)質(zhì)量和教學(xué)效率。

(二)提高學(xué)生學(xué)習(xí)興趣

傳統(tǒng)教學(xué)方式下的邏輯學(xué)教學(xué)過(guò)程，教師很容易采用灌輸式的理論闡述方法傳授知識(shí)，而忽視學(xué)生的興趣和好奇心，不重視學(xué)生學(xué)習(xí)的主體地位。采用邏輯推理實(shí)驗(yàn)課的教學(xué)方式，教師結(jié)合教學(xué)內(nèi)容演示并教授學(xué)生使用相應(yīng)的邏輯軟件，使學(xué)生轉(zhuǎn)化為教學(xué)活動(dòng)中的主體。借助于邏輯軟件，教學(xué)活動(dòng)中的主體和客體相互轉(zhuǎn)化，教師能夠采用啟發(fā)式、參與式和探究式為主的教學(xué)方法，摒棄枯燥的講授法。通過(guò)人機(jī)交互式操作，學(xué)生能夠充分發(fā)揮主觀能動(dòng)性，主動(dòng)地探索并獲取自己所需要的知識(shí)，快速掌握比較抽象的邏輯方法和規(guī)律，使學(xué)習(xí)變得輕松有趣，大大提高了學(xué)習(xí)興趣。

(三)增強(qiáng)大學(xué)生邏輯思維素養(yǎng)

作為一門研究人的思維及其規(guī)律的工具學(xué)科，邏輯教育的目的就是為了提高人們的思維能力，提高人們運(yùn)用邏輯工具解決現(xiàn)實(shí)生活中各種問(wèn)題的能力。隨著現(xiàn)代科學(xué)技術(shù)的發(fā)展，以互聯(lián)網(wǎng)、多媒體技術(shù)、數(shù)學(xué)電視、手機(jī)等為代表的新媒體深刻地改變著人們的生活方式、思維方式和價(jià)值觀念。邏輯教學(xué)軟件也是現(xiàn)代科學(xué)技術(shù)的產(chǎn)物，是邏輯教育的一種技術(shù)手段，有助于培養(yǎng)大學(xué)生邏輯思維能力。邏輯推理實(shí)驗(yàn)課是邏輯理論課的擴(kuò)展，利用邏輯軟件，學(xué)生創(chuàng)造性地運(yùn)用邏輯工具去分析問(wèn)題、解決問(wèn)題并驗(yàn)證問(wèn)題。邏輯軟件一般預(yù)設(shè)有大量的練習(xí)或游戲，學(xué)生進(jìn)行反復(fù)的操作和訓(xùn)練，由“生動(dòng)的直觀”上升到“抽象的思維”，學(xué)到的邏輯知識(shí)和方法逐漸轉(zhuǎn)化為邏輯思維素養(yǎng)，樹(shù)立起正確的邏輯觀念，形成正確的思維習(xí)慣。

(四)促進(jìn)邏輯教學(xué)現(xiàn)代化的發(fā)展

我國(guó)邏輯學(xué)界提出的邏輯教學(xué)和研究要現(xiàn)代化，是在中國(guó)的高等教育中，普及邏輯學(xué)課程，使現(xiàn)代邏輯逐漸成為邏輯教學(xué)的主流，與國(guó)際邏輯教學(xué)和研究水平全面接軌。邏輯教學(xué)軟件是現(xiàn)代化的教育技術(shù)手段，促進(jìn)了邏輯專業(yè)教育觀念的轉(zhuǎn)變、教學(xué)內(nèi)容的創(chuàng)新和教學(xué)方法的改革。相比傳統(tǒng)邏輯軟件來(lái)說(shuō)，國(guó)外研發(fā)的數(shù)理邏輯和模態(tài)邏輯軟件更多，也比較完善。利用這些軟件，邏輯學(xué)中許多抽象的理論能生動(dòng)、形象地顯示，學(xué)生能很容易地掌握現(xiàn)代邏輯的核心部分，從而使現(xiàn)代邏輯教學(xué)富有成效。目前，國(guó)內(nèi)研發(fā)的邏輯軟件寥寥可數(shù)，因此借鑒國(guó)外先進(jìn)的教學(xué)技術(shù)和教學(xué)理念，將有助于縮短我國(guó)與國(guó)外邏輯教學(xué)和研究的差距。邏輯教育技術(shù)手段的革新，勢(shì)必推動(dòng)整個(gè)邏輯教學(xué)和研究的現(xiàn)代化。

［1］李娜．邏輯學(xué)實(shí)驗(yàn)教程［M］．天津：南開(kāi)大學(xué)出版社，2012．

［2］王湘云．基于謂詞邏輯的知識(shí)表示和知識(shí)推理及在Prolog中的實(shí)現(xiàn)［D］．天津：南開(kāi)大學(xué)，2008．

［3］李娜，孫雯．國(guó)外邏輯學(xué)習(xí)軟件初探——兼談國(guó)內(nèi)邏輯學(xué)習(xí)軟件情況［J］．邏輯學(xué)研究，2011(4)：98-110．

［4］李娜．?dāng)?shù)理邏輯實(shí)驗(yàn)教程［M］．武漢：武漢大學(xué)出版社，2010．

［5］王湘云．基于范疇的非良基理論及其應(yīng)用研究［D］．天津：南開(kāi)大學(xué)，2011．

［6］Akman V，Pakkan M．Hypersolver：A graphical tool for commonsense set Theory［G］//Gün L，?nvural R，Gelenbe E，et al．Proceedings of Eight International Symposium on Computer and Information Sciences．Turkey：Istanbul，1993：436-443．

(責(zé)任編輯 張佑法)

Logic-teaching Software and its Effectiveness

WANG Xiang-yun
(North China University ofWater Resources and Electric Power，Zhengzhou 450011，China)

As an importantmeans ofmodern educational technology，the logic-teaching software plays an essential role in the process of logic education．The use of logic-teaching software can not only enhance the quality and efficiency of teaching and promote the development of themodernization of logic-teaching，but also it can help the students have a better understanding of logic thinking and master the logicmethods easily and efficiently．This papermainly introduces some international popular logicteaching software aswell as the use and effectiveness of logic software in domestic logic-teaching．

logic-teaching software;modernization of educational technology;modernization of logicteaching;effectiveness

B81;G642

A

1674-8425(2014)07-0028-06

10．3969/j．issn．1674-8425(s)．2014．07．006

2014-01-08

王湘云(1977—)，女，河南開(kāi)封人，講師，哲學(xué)博士，研究方向:現(xiàn)代邏輯。

王湘云．邏輯教學(xué)軟件及其實(shí)效性研究［J］．重慶理工大學(xué)學(xué)報(bào):社會(huì)科學(xué)，2014(7):28-33．

format:WANG Xiang-yun．Logic-teaching Software and its Effectiveness［J］．Journal of Chongqing University of Technology:Social Science，2014(7):28-33．