王湘云

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

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

王湘云

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

亞里士多德詞項邏輯是由德國邏輯學(xué)家克勞斯·格拉斯霍夫(Klaus Glashoff)于2004年開發(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年開發(fā)的一個在線教學(xué)平臺。其中的范疇邏輯計算器(Categorical Logic)也是一款關(guān)于三段論學(xué)習(xí)的傳統(tǒng)邏輯軟件。該軟件對傳統(tǒng)邏輯性質(zhì)判斷中的主項和謂項之間的外延關(guān)系，用構(gòu)造出的文恩圖做出判斷和檢驗，還可以進行直言推理、三段論推理、連鎖推理和省略式三段論推理。

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

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

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

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

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

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

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

柏拉圖是美國得克薩斯大學(xué)的羅伯特·昆斯(Robert C．Koons)開發(fā)的邏輯在線教學(xué)平臺，用于形式邏輯基礎(chǔ)課程的學(xué)習(xí)，內(nèi)容包括在線課程、軟件下載、學(xué)習(xí)指南、專業(yè)詞典等。柏拉圖程序能夠使用戶構(gòu)造命題演算和謂詞演算形式語言中的證明，也可用來構(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)開發(fā)的通向邏輯之門在線平臺集一些基于網(wǎng)絡(luò)的邏輯程序為一體，并提供了一些邏輯函數(shù)，如真值表、范式、證明檢驗、證明構(gòu)造等。服務(wù)器端函數(shù)(Server-side Functions)用來計算經(jīng)典二值命題邏輯的公式，由真值表、重言式檢驗、圖解表達式樹、文本表達式樹、合取范式、典范合取范式、析取范式、典范析取范式等一系列函數(shù)組成。證明生成器(Proof Builder)是能夠交互式地構(gòu)造證明的程序。證明檢查器(Proof Checker)可以檢驗用戶提交的證明。自動定理證明器(Automated Theorem Prover)適用于經(jīng)典的謂詞邏輯，可以自動地推出有效論證，直接在服務(wù)器端上執(zhí)行。

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

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

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

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

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

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

10．超證明(Hyperproof)

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

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

11．超求解器(Hypersolver)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

［1］李娜．邏輯學(xué)實驗教程［M］．天津：南開大學(xué)出版社，2012．

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

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

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

［5］王湘云．基于范疇的非良基理論及其應(yīng)用研究［D］．天津：南開大學(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—)，女，河南開封人，講師，哲學(xué)博士，研究方向:現(xiàn)代邏輯。

王湘云．邏輯教學(xué)軟件及其實效性研究［J］．重慶理工大學(xué)學(xué)報:社會科學(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．