邏輯教學軟件及其實效性研究

王湘云

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

邏輯教學軟件及其實效性研究

王湘云

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

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

邏輯教學軟件;教育技術現代化;邏輯教學現代化;實效性

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

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

一、邏輯教學軟件產生的背景

邏輯學和計算機的關系非常密切，特別是現代邏輯的研究方法和研究成果在計算機科學各領域都有廣泛的應用。

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

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

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

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

二、邏輯教學軟件的研究狀況

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

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

國外對邏輯軟件的研發已經取得了豐富的成果。早在1980年，美國斯坦福大學語言與信息研究中心(CSLI)就研發了一系列具有開創性和實效性的邏輯應用軟件，用于本科生數理邏輯課程的教學和研究。目前，在國外的大學邏輯學教學中，較多地使用了邏輯軟件，特別是一些現代邏輯軟件的應用已經相當地成熟和完善。

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

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

亞里士多德詞項邏輯是由德國邏輯學家克勞斯·格拉斯霍夫(Klaus Glashoff)于2004年開發的一款傳統邏輯軟件。這款邏輯在線軟件的主要功能是學習亞里士多德三段論邏輯的自然演繹系統。該軟件預設了全部的三段論演繹規則，輸入三段論的前提，并選擇相應的有效論式，執行后就可以直接得到結論。

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

邏輯工具箱是約翰·薩埃蒂(John Saetti)于2009年開發的一個在線教學平臺。其中的范疇邏輯計算器(Categorical Logic)也是一款關于三段論學習的傳統邏輯軟件。該軟件對傳統邏輯性質判斷中的主項和謂項之間的外延關系，用構造出的文恩圖做出判斷和檢驗，還可以進行直言推理、三段論推理、連鎖推理和省略式三段論推理。

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

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

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

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

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

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

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

柏拉圖是美國得克薩斯大學的羅伯特·昆斯(Robert C．Koons)開發的邏輯在線教學平臺，用于形式邏輯基礎課程的學習，內容包括在線課程、軟件下載、學習指南、專業詞典等。柏拉圖程序能夠使用戶構造命題演算和謂詞演算形式語言中的證明，也可用來構造包括集合論部分在內的形式化的數學證明。

7．通向邏輯之門(Gateway to Logic)⑦網址:http://logik．phl．univie．ac．at/～chris/gateway/formularuk．htm l

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

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

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

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

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

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

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

10．超證明(Hyperproof)

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

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

11．超求解器(Hypersolver)

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

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

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

(二)國內邏輯教學軟件的研究

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

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

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

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

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

三、邏輯教學軟件的實效性

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

(一)提高教學質量和教學效率

盡管邏輯學理論的研究取得了顯著的成果，但邏輯學教學的狀況并不樂觀，特別是在我國高等教育中。近幾年來，邏輯通識教育面臨各種困境，有關邏輯學教學方面的研究成果很少。邏輯教學軟件的產生和發展及其在課堂教學中的逐漸應用，促使了邏輯教學水平的不斷提高。邏輯學較其他基礎課而言，難學、難懂、難掌握，尤其是現代邏輯的內容更加抽象。基于網絡和計算機平臺的邏輯軟件具有可視化的界面，形象、直觀、生動、具體，而且內容豐富，可以容納大量教學材料或實例。許多繁瑣的、重復的、形式化的推理演算和驗證工作，甚至教師需要評分的習題，都可以交給邏輯軟件來完成，既節省時間，又減少錯誤，能夠有效地提高教學質量和教學效率。

(二)提高學生學習興趣

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

(三)增強大學生邏輯思維素養

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

(四)促進邏輯教學現代化的發展

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

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

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

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

［4］李娜．數理邏輯實驗教程［M］．武漢：武漢大學出版社，2010．

［5］王湘云．基于范疇的非良基理論及其應用研究［D］．天津：南開大學，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．

(責任編輯 張佑法)

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—)，女，河南開封人，講師，哲學博士，研究方向:現代邏輯。

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