邏輯教學(xué)軟件的研究狀況及其實(shí)效性,邏輯學(xué)論文

邏輯教學(xué)軟件的研究狀況及其實(shí)效性,邏輯學(xué)論文20世紀(jì)90年代以來,一批具有現(xiàn)代特色的邏輯學(xué)教學(xué)資料應(yīng)運(yùn)而生,邏輯教學(xué)探尋求索與改革成果豐富.隨著當(dāng)代數(shù)字和信息技術(shù)的飛速發(fā)展,在邏輯教學(xué)中運(yùn)用新媒體和當(dāng)代教育技術(shù)的手段也日趨成熟.這些實(shí)踐促進(jìn)了邏輯學(xué)的教學(xué)改革,提升了邏輯學(xué)的教學(xué)水平,也加強(qiáng)了邏輯學(xué)的教學(xué)效果.作為當(dāng)代化教育技術(shù)的一個(gè)重要手段,邏輯教學(xué)軟件在邏輯教育經(jīng)過中的作用越來越顯著.邏輯教學(xué)軟件的使用,有利于學(xué)生更好地理解邏輯的思想,更有效地把握邏輯的方式方法[1],給高校邏輯學(xué)教育帶來了新的機(jī)遇和挑戰(zhàn).一、邏輯教學(xué)軟件產(chǎn)生的背景邏輯學(xué)和計(jì)算機(jī)的關(guān)系非常密切,十分是當(dāng)代邏輯的研究方式方法和研究成果在計(jì)算機(jī)科學(xué)各領(lǐng)域都有廣泛的應(yīng)用.12世紀(jì)末13世紀(jì)初,西班牙邏輯學(xué)家羅門盧樂(RomenLuee)提出了制造可解決各種問題的通用邏輯機(jī),初步揭示了人類思維與計(jì)算可同一的思想.17世紀(jì),德國數(shù)學(xué)家和哲學(xué)家萊布尼茲(G.W.Leibniz)改良了帕斯卡(B.Pascal)的加法數(shù)字計(jì)算器,做出了四則運(yùn)算的手搖計(jì)算器,并提出了通用符號(hào)和推理計(jì)算的思想,使形式邏輯符號(hào)化,這能夠講是機(jī)器思維研究的萌芽.19世紀(jì),英國數(shù)學(xué)家布爾(G.Boole)創(chuàng)立了布爾代數(shù),第一次用符號(hào)語言描繪敘述了思維的基本推理法則,真正使邏輯代數(shù)化.布爾系統(tǒng)奠定了當(dāng)代形式邏輯研究的基礎(chǔ).20世紀(jì)初期,懷特海(A.N.Whitehead)和羅素(B.A.W.Russel)在合著的(數(shù)學(xué)原理〕(1910-1913)中,提出了從純形式系統(tǒng)的角度(即機(jī)械角度)來處理數(shù)學(xué)推理的方式方法,為數(shù)學(xué)推理在計(jì)算機(jī)上的自動(dòng)化實(shí)現(xiàn)奠定了理論基礎(chǔ).他們開發(fā)的邏輯句法和形式推理規(guī)則是自動(dòng)定理證明系統(tǒng)的基礎(chǔ),也是人工智能的理論基礎(chǔ).1937年,英國數(shù)學(xué)家圖靈(A.M.Turing)建立了描繪敘述算法的機(jī)械性思維經(jīng)過,提出了理想計(jì)算機(jī)模型(即圖靈機(jī)),創(chuàng)立了自動(dòng)機(jī)理論,奠定了整個(gè)計(jì)算機(jī)科學(xué)的理論基礎(chǔ).據(jù)此,1945年匈牙利數(shù)學(xué)家馮諾依曼(JohnVonNeumann)提出了存儲(chǔ)程序的思想,并建立了通用電子數(shù)字計(jì)算機(jī)的馮諾依曼型體系構(gòu)造;1946年美國的莫克利(J.W.Mauchly)和?？颂?J.P.Eckert)成功研制出世界上第一臺(tái)通用電子數(shù)學(xué)計(jì)算機(jī)ENIAC[2].20世紀(jì)中期,人們開場設(shè)想用計(jì)算機(jī)進(jìn)行邏輯推理.1956年,國際著名的邏輯學(xué)家、數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家紐厄爾(A.Newell)和西蒙(H.A.Si-mon)等人首先獲得突破,他們編制的模擬人的啟發(fā)式搜索問題解決的計(jì)算機(jī)程序邏輯理論家證明了羅素和懷德海合著的(數(shù)學(xué)原理〕第二章中的38條邏輯推理.后來經(jīng)過改良,又證明了該章的全部52條邏輯推理.此后,世界著名邏輯學(xué)家美籍華人王浩教授在IBM-704計(jì)算機(jī)上以3~5分鐘的時(shí)間證明了(數(shù)學(xué)原理〕中有關(guān)命題演算的全部220條邏輯推理,并且還證明了該書中帶等詞的謂詞演算的150條邏輯推理的85%.不久,他僅用8.4分鐘的時(shí)間證明了以上全部邏輯推理[3].同一時(shí)期,我們國家著名數(shù)學(xué)家吳文俊教授也在自動(dòng)定理證明方面做出了突出的奉獻(xiàn),他提出的把幾何問題代數(shù)化的方式方法被國際上的學(xué)者稱為吳方式方法.隨著計(jì)算機(jī)科學(xué)技術(shù)的迅速發(fā)展,自動(dòng)推理的作用顯得越來越重要,很多邏輯學(xué)家嘗試使用計(jì)算機(jī)來模擬邏輯的思想和方式方法,進(jìn)而研發(fā)了一系列的邏輯軟件,推動(dòng)了邏輯學(xué)教育技術(shù)的當(dāng)代化.當(dāng)代信息技術(shù)帶來了當(dāng)代化的教學(xué)手段,也對(duì)傳統(tǒng)的教學(xué)方式和教學(xué)手段進(jìn)行了革新.同多媒體課件、電子學(xué)習(xí)資源、網(wǎng)絡(luò)課程等當(dāng)代化的教育技術(shù)手段一樣,邏輯教學(xué)軟件在邏輯教學(xué)經(jīng)過也發(fā)揮著特別重要的作用.進(jìn)入21世紀(jì),邏輯軟件的開發(fā)及在邏輯教學(xué)中的應(yīng)用逐步成為邏輯教育經(jīng)過中極為重要的一個(gè)環(huán)節(jié).2000年、2006年和2018年,在西班牙的薩拉曼卡大學(xué),分別召開了3次關(guān)于邏輯教學(xué)工具的國際性學(xué)術(shù)研討會(huì).這3次會(huì)議將邏輯教學(xué)軟件的開發(fā)和使用作為重要議題來討論,對(duì)邏輯軟件的發(fā)展前景、邏輯教學(xué)軟件在邏輯教學(xué)中的作用等詳細(xì)問題進(jìn)行了深切進(jìn)入的研究,引起了邏輯學(xué)界對(duì)邏輯教學(xué)軟件的廣泛興趣和重視,有力地推動(dòng)了邏輯教學(xué)軟件的發(fā)展.二、邏輯教學(xué)軟件的研究狀況從操作形式來看,邏輯軟件主要有計(jì)算機(jī)網(wǎng)絡(luò)在線邏輯軟件和計(jì)算機(jī)程序設(shè)計(jì)邏輯軟件兩類.計(jì)算機(jī)網(wǎng)絡(luò)在線邏輯軟件是基于萬維網(wǎng)的,有邏輯教學(xué)網(wǎng)絡(luò)平臺(tái)的支持,并由軟件供給商提供程序在線服務(wù).在線邏輯軟件有對(duì)應(yīng)的網(wǎng)絡(luò)鏈接,學(xué)習(xí)者直接在網(wǎng)絡(luò)界面下使用,能夠進(jìn)行互動(dòng)練習(xí),操作簡便.計(jì)算機(jī)程序設(shè)計(jì)邏輯軟件是用某種程序設(shè)計(jì)語言編寫,運(yùn)行于Windows或Mac等操作系統(tǒng)上的應(yīng)用軟件.程序設(shè)計(jì)邏輯軟件由用戶安裝在計(jì)算機(jī)中,執(zhí)行特定的功能,操作具有獨(dú)立性.根據(jù)形式邏輯的分類,邏輯軟件可以分為傳統(tǒng)邏輯軟件、數(shù)理邏輯軟件、哲學(xué)邏輯軟件等等.(一)國外邏輯教學(xué)軟件的研究國外對(duì)邏輯軟件的研發(fā)已經(jīng)獲得了豐富的成果.早在1980年,美國斯坦福大學(xué)語言與信息研究中心(CSLI)就研發(fā)了一系列具有創(chuàng)始性和實(shí)效性的邏輯應(yīng)用軟件,用于本科生數(shù)理邏輯課程的教學(xué)和研究.當(dāng)前,在國外的大學(xué)邏輯學(xué)教學(xué)中,較多地使用了邏輯軟件,十分是一些當(dāng)代邏輯軟件的應(yīng)用已經(jīng)相當(dāng)?shù)爻墒旌屯晟?我們參考國外的邏輯教育網(wǎng)站,扼要介紹一些流行且實(shí)用的邏輯軟件.1.亞里士多德詞項(xiàng)邏輯(ComputationalAristo-telianTermLogic)①亞里士多德詞項(xiàng)邏輯是由德國邏輯學(xué)家克勞斯格拉斯霍夫(KlausGlashoff)于2004年開發(fā)的一款傳統(tǒng)邏輯軟件.這款邏輯在線軟件的主要功能是學(xué)習(xí)亞里士多德三段論邏輯的自然演繹系統(tǒng).該軟件預(yù)設(shè)了全部的三段論演繹規(guī)則,輸入三段論的前提,并選擇相應(yīng)的有效論式,執(zhí)行后就能夠直接得到結(jié)論.2.邏輯工具箱(LogicToolbox)②邏輯工具箱是約翰薩埃蒂(JohnSaetti)于2018年開發(fā)的一個(gè)在線教學(xué)平臺(tái).華而不實(shí)的范疇邏輯計(jì)算器(CategoricalLogic)也是一款關(guān)于三段論學(xué)習(xí)的傳統(tǒng)邏輯軟件.該軟件對(duì)傳統(tǒng)邏輯性質(zhì)判定中的主項(xiàng)和謂項(xiàng)之間的外延關(guān)系,用構(gòu)造出的文恩圖做出判定和檢驗(yàn),還能夠進(jìn)行直言推理、三段論推理、連鎖推理和省略式三段論推理.3.樹證明發(fā)生器(TreeProofGenerater)③樹證明發(fā)生器是由沃爾夫?qū)?WolfgangSchwarz)于2007年11月發(fā)布的一個(gè)利用JavaS-cript程序設(shè)計(jì)的在線邏輯軟件.樹證明的方式方法也稱作語義表,是檢查各種邏輯公式有效性的一種有效算法.這款數(shù)理邏輯軟件為經(jīng)典的命題邏輯和不含等詞的謂詞邏輯提供語義表.用戶只需輸入要驗(yàn)證的、有效的命題公式或謂詞公式,系統(tǒng)就會(huì)自動(dòng)生成一棵證明樹或者給出反模型的證明.4.邏輯動(dòng)畫入門(IntroductoryLogicAnima-tions)④1988-1999年,由荷蘭阿姆斯特丹大學(xué)的賈恩(JanJaspars)等人開發(fā)的邏輯動(dòng)畫入門也是利用JavaScript程序設(shè)計(jì)的一個(gè)在線邏輯軟件.該軟件能夠?qū)A(chǔ)數(shù)理邏輯和哲學(xué)邏輯的形式演算進(jìn)行互動(dòng)訓(xùn)練,包括命題邏輯、謂詞邏輯、模態(tài)邏輯、動(dòng)態(tài)邏輯和圖靈機(jī)5個(gè)功能模塊,每一個(gè)功能模塊又由若干子程序組成.例如,命題邏輯功能模塊下的子程序:命題計(jì)算器(propositionalcalcu-lator)可斷定一個(gè)命題邏輯公式能否是重言式、矛盾式或可知足式,以及該公式真值為真或假時(shí),其命題變項(xiàng)的真值組合.謂詞邏輯功能模塊下的子程序:謂詞計(jì)算器(predicatecalculator)用來計(jì)算給定模型上的謂詞邏輯公式的結(jié)果,并查找自由變項(xiàng)的正反實(shí)例.模態(tài)邏輯功能模塊的子程序:可能世界計(jì)算器(possibleworldcalculator)可在一個(gè)給定的克里普克(Kripke)模型中計(jì)算出哪些世界能夠驗(yàn)證輸入的模態(tài)公式.動(dòng)態(tài)邏輯功能模塊下的子程序:傳遞計(jì)算器(transitioncalculator)能夠計(jì)算一個(gè)給定正則表示出式的傳遞外延.5.交互式邏輯程序(InteractiveLogicPro-grams)⑤交互式邏輯程序是加拿大滑鐵盧大學(xué)的斯坦利貝爾雷斯(StanleyN.Burris)開發(fā)的在線教學(xué)平臺(tái),包括真值表(TruthTables)、命題聯(lián)合詞(PropositionalConnectives)、戴維斯-帕特南程序(Davis-Putnamprocedure)、合一算法(UnificationAlgorithm)、自動(dòng)定理證明器(AutomatedTheoremProver)等一系列邏輯軟件.例如,命題聯(lián)合詞程序可令用戶選擇任意的常項(xiàng)0、1,否認(rèn)詞﹁和16進(jìn)制的二元聯(lián)合詞,然后驗(yàn)證哪些聯(lián)合詞能夠由已選定的聯(lián)合詞得到.戴維斯-帕特南程序允許用戶最多項(xiàng)選擇擇10個(gè)子句,然后后臺(tái)運(yùn)用戴維斯-帕特南方式方法確定所選子句集能否是可知足的.合一算法程序允許用戶選擇兩個(gè)前綴形式的項(xiàng),然后找出它們的一致置換,等等.6.柏拉圖(Plato)⑥柏拉圖是美國得克薩斯大學(xué)的羅伯特昆斯(RobertC.Koons)開發(fā)的邏輯在線教學(xué)平臺(tái),用于形式邏輯基礎(chǔ)課程的學(xué)習(xí),內(nèi)容包括在線課程、軟件下載、學(xué)習(xí)指南、專業(yè)詞典等.柏拉圖程序能夠使用戶構(gòu)造命題演算和謂詞演算形式語言中的證明,可以用來構(gòu)造包括集合論部分在內(nèi)的形式化的數(shù)學(xué)證明.7.通向邏輯之門(GatewaytoLogic)⑦奧地利維也納大學(xué)的克里斯汀戈特沙爾(ChristianGottschall)開發(fā)的通向邏輯之門在線平臺(tái)集一些基于網(wǎng)絡(luò)的邏輯程序?yàn)橐惑w,并提供了一些邏輯函數(shù),如真值表、范式、證明檢驗(yàn)、證明構(gòu)造等.服務(wù)器端函數(shù)(Server-sideFunctions)用來計(jì)算經(jīng)典二值命題邏輯的公式,由真值表、重言式檢驗(yàn)、圖解表示出式樹、文本表示出式樹、合取范式、典范合取范式、析取范式、典范析取范式等一系列函數(shù)組成.證明生成器(ProofBuilder)是能夠交互式地構(gòu)造證明的程序.證明檢查器(ProofCheck-er)能夠檢驗(yàn)用戶提交的證明.自動(dòng)定理證明器(AutomatedTheoremProver)適用于經(jīng)典的謂詞邏輯,能夠自動(dòng)地推出有效論證,直接在服務(wù)器端上執(zhí)行.8.阿卡網(wǎng)絡(luò)平臺(tái)(AkkafliestheWeb)①荷蘭阿姆斯特丹大學(xué)的萊克斯(LexHen-driks)于1998年開發(fā)的阿卡網(wǎng)絡(luò)平臺(tái)能夠檢驗(yàn)一些邏輯系統(tǒng)中公式的可證明性和模型中公式的有效性,為動(dòng)態(tài)邏輯繪制并編輯克里普克模型,以及用計(jì)算機(jī)測定邏輯語義圖.阿卡是對(duì)克里普克模型進(jìn)行定理測試和模型測試的工具,提供克里普克模型編輯器并且支持模型測試,還可提供附加的服務(wù),如語義圖的構(gòu)造.除此之外,瑞士伯爾尼大學(xué)開發(fā)的邏輯工作臺(tái)(TheLogicsWorkbench),②美國德克薩斯州農(nóng)業(yè)機(jī)械大學(xué)開發(fā)的邏輯后臺(tái)程序和課堂測驗(yàn)(LogicDaemonandQuizmaster),③美國猶他大學(xué)開發(fā)的表示出式計(jì)算器(ExpressionEvaluator)④等等,都是用于形式邏輯學(xué)習(xí)的在線邏輯教學(xué)平臺(tái).9.語言、證明和邏輯(Language,ProofandLog-ic)語言、證明和邏輯教學(xué)軟件包,簡稱LPL,是美國斯坦福大學(xué)語言與信息研究中心(CSLI)研發(fā)的一套專門用于一階邏輯語言學(xué)習(xí)的計(jì)算機(jī)程序組件.該教學(xué)軟件包與美國邏輯學(xué)家、印第安那大學(xué)的巴威斯(JonBarwise)及其在斯坦福大學(xué)語言與信息研究中心的同事艾克曼迪(JohnEtchemendy)合著的(一階邏輯的語言〕,以及他們二人合著的改良版本(語言、證明和邏輯〕二書配套使用[4].LPL軟件包是當(dāng)前最為成熟、功能上愈加完善的一組數(shù)理邏輯學(xué)習(xí)軟件,包括布爾(Boole)、費(fèi)奇(Fitch)、塔斯基的世界(TarskisWorld)3個(gè)邏輯程序和一個(gè)基于互聯(lián)網(wǎng)的分等級(jí)服務(wù):提交(Submit).這些程序能在計(jì)算機(jī)操作系統(tǒng)Windows或Mac下使用.布爾程序用于構(gòu)造邏輯公式的真值表.其最大的特點(diǎn)就是對(duì)公式中所含命題變項(xiàng)的個(gè)數(shù)沒有限制并能同時(shí)構(gòu)造若干個(gè)命題的真值表.塔斯基的世界程序用于學(xué)習(xí)一階語言及其語義.用戶能夠在該程序設(shè)計(jì)的三維空間里使用和改造已有的世界或創(chuàng)造新的世界,編寫一階邏輯的語句,判定它們的真值,還能夠通過做游戲,檢驗(yàn)自個(gè)對(duì)語句真值的判定能否正確,進(jìn)而把握邏輯聯(lián)合詞和量詞的用法.費(fèi)奇程序用于構(gòu)造自然推理系統(tǒng)F下的形式證明.用戶能夠運(yùn)用相應(yīng)的推理規(guī)則分步驟驗(yàn)證一階公式的形式證明.提交程序用于網(wǎng)上提交作業(yè).學(xué)生的作業(yè)能夠直接遞交給評(píng)分服務(wù)器(GradeGrinder),它將給作業(yè)評(píng)分并將結(jié)果發(fā)送給學(xué)生及導(dǎo)師.10.超證明(Hyperproof)超證明也是由巴威斯和艾克曼迪共同研發(fā)的一款用于分析謂詞邏輯自然演繹形式的推理經(jīng)過的程序軟件.這款程序僅適用于蘋果機(jī)型,與二人1994出版的(超證明〕一書配套使用.超證明是分析推論和證明經(jīng)過的規(guī)則的一個(gè)學(xué)習(xí)系統(tǒng),與傳統(tǒng)的對(duì)一階邏輯處理的方式不同,它包含圖形信息和句子信息,綜合不同的信息形式,描繪敘述出一系列的推理規(guī)則.這種方式能夠使學(xué)生集中于證明內(nèi)容的信息,而不是句子的語法構(gòu)造,進(jìn)而利用一種直觀的證明系統(tǒng),學(xué)會(huì)構(gòu)建后承和非后承的證明,將標(biāo)準(zhǔn)的句法規(guī)則擴(kuò)展為用圖形表示的合并信息.超證明軟件能夠檢查每一證明類型的邏輯有效性,適用于各種自然演繹形式的證明系統(tǒng),包括巴威斯和艾克曼迪的一階邏輯語言的系統(tǒng).還適用于塔斯基的世界程序,能構(gòu)造和檢查塔斯基的世界語言中的證明.它允許用戶將圖形表示的信息和圖形相合適的演繹技術(shù)、句子和語法規(guī)則組合,對(duì)塔斯基的世界中的塊世界進(jìn)行推理,使得學(xué)習(xí)一階邏輯具有極大的樂趣.11.超求解器(Hypersolver)超求解器是由土爾其比爾肯大學(xué)的阿克曼(V.Akman)和土爾其海峽大學(xué)的帕克坎(M.Pak-kan)于1993年研發(fā)的一款利用解引理在非良基集合全域中解方程的程序軟件.非良基集合(Non-well-foundedsets),也稱超集(Hypersets),是具有循環(huán)性質(zhì)或無窮降鏈性質(zhì)的集合.1987年,美國著名邏輯學(xué)家巴威斯(J.Barwise)和艾切曼迪(J.Etchemendy)為了證明非良基集合的存在性,引入解引理講明每個(gè)方程組有唯一解,即把集合看作方程組的解.為了得到更為豐富的集合全域,保證非良基集合的存在,以便對(duì)各種循環(huán)現(xiàn)象做出解釋,能夠在標(biāo)準(zhǔn)集合論中用非良基公理替換良基公理,進(jìn)而得到非良基集合論.而非良基集合論給出了一套完備的工具能夠刻畫現(xiàn)實(shí)世界中各種各樣的循環(huán)問題.就此而言,非良基集合論的作用和影響已經(jīng)遠(yuǎn)遠(yuǎn)超出了經(jīng)典的集合論ZFC[5].解引理是非良基集合論的特色.超求解程序,是一個(gè)基于解引理的、獨(dú)立操作的程序,能夠?qū)Ω鶕?jù)集合定義的方程組進(jìn)行求解.它具有內(nèi)置的圖解功能,能夠顯示出描繪敘述用戶輸入方程以及這些方程解的圖.超求解器的用戶接口,稱作命令接口.用戶輸入有效的一個(gè)文件,文件中的每一行都是一個(gè)方程,文件被送到語法解析器轉(zhuǎn)變?yōu)長isp(列表處理語言)形式,并檢驗(yàn)?zāi)芊穹陷斎胍?之后,超求解器的解算器將解引理應(yīng)用到所輸入的方程組,進(jìn)行求解.接下來是圖顯示部件的調(diào)用,這一部件輸入解算器產(chǎn)生的方程組的解,最后由圖繪制程序描繪敘述出方程組的解決方案圖并顯示在圖顯示窗中.除了具有數(shù)學(xué)上的重要性和精到準(zhǔn)確性之外,超求解器還提供了刻畫各種循環(huán)現(xiàn)象的一種有趣的方式方法.在人工智能領(lǐng)域中,信息能夠以方程組的形式來布置,因此該程序是進(jìn)行常識(shí)推理的一個(gè)非常有用的實(shí)用工具.超求解程序具有一般的語法分析器和直觀的圖形界面,也是數(shù)理邏輯的重要工具程序之一.超求解程序的施行,使得利用解引理模型化循環(huán)的現(xiàn)象同計(jì)算機(jī)自動(dòng)化求解問題嚴(yán)密地結(jié)合起來,極具應(yīng)用價(jià)值[6].(二)國內(nèi)邏輯教學(xué)軟件的研究國內(nèi)對(duì)邏輯教學(xué)軟件的研究相對(duì)國外而言還特別薄弱,剛剛進(jìn)入起步階段.2007年5月,南開大學(xué)哲學(xué)院建設(shè)了國內(nèi)第一個(gè)邏輯推理實(shí)驗(yàn)室,也是當(dāng)前國內(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é)中引入當(dāng)代化技術(shù),逐步與國際邏輯學(xué)教學(xué)接軌.最近幾年來,實(shí)驗(yàn)室負(fù)責(zé)人李娜教授及成員在數(shù)理邏輯課程的教學(xué)經(jīng)過中,將邏輯軟件同邏輯學(xué)教學(xué)材料、教學(xué)課件一樣作為教學(xué)工具來使用.實(shí)驗(yàn)室使用的邏輯軟件主要是從國外購買的教學(xué)軟件包,以及國外的網(wǎng)絡(luò)在線教學(xué)軟件.除此之外,實(shí)驗(yàn)室還開發(fā)了兩個(gè)教學(xué)軟件,一個(gè)是能夠快速構(gòu)造真值表、計(jì)算命題公式真值的邏輯軟件:邏輯運(yùn)算3.0.①這款軟件有中英兩個(gè)版本,適用于Win-dows操作平臺(tái),能夠計(jì)算不超過6個(gè)命題變項(xiàng)的命題公式的真值,并能列出不超過6個(gè)命題變項(xiàng)的命題公式的真值表.另一個(gè)是數(shù)理邏輯學(xué)習(xí)詞典.固然這兩個(gè)軟件的功能相對(duì)簡單且還不夠完善,但總算打破了國內(nèi)邏輯學(xué)軟件的研發(fā)一直是空白的境況.李娜教授編寫出版了兩本邏輯實(shí)驗(yàn)教學(xué)資料:(數(shù)理邏輯實(shí)驗(yàn)教程〕和(邏輯學(xué)實(shí)驗(yàn)教程〕.前者主要針對(duì)數(shù)理邏輯的學(xué)習(xí)及數(shù)理邏輯軟件的使用,后者是包括亞里士多德三段論邏輯、數(shù)理邏輯和哲學(xué)邏輯(模態(tài)邏輯)的完全形式化推理的實(shí)驗(yàn)教學(xué)資料.當(dāng)前,實(shí)驗(yàn)室還在繼續(xù)建設(shè)當(dāng)中,實(shí)驗(yàn)室與臺(tái)灣東吳大學(xué)的林正弘教授就國際上一些邏輯教學(xué)軟件的使用情況進(jìn)行了溝通;2008年10月,世界邏輯學(xué)家本特姆(JohanvanBenthem)先生到實(shí)驗(yàn)室參觀和溝通,并對(duì)邏輯動(dòng)畫入門軟件中的更新和驗(yàn)算器進(jìn)行了深切進(jìn)入的講解;2018年10月7日,南開大學(xué)哲學(xué)院召開了邏輯學(xué)開放教學(xué)與網(wǎng)絡(luò)應(yīng)用軟件國際研討會(huì),來自美國斯坦福大學(xué)、荷蘭阿姆斯特丹大學(xué)、西班牙塞維利亞大學(xué)、印度晨奈數(shù)學(xué)研究所、新西蘭奧克蘭大學(xué),以及清華大學(xué)、北京大學(xué)、浙江大學(xué)、中山大學(xué)、南開大學(xué)的學(xué)者就邏輯教學(xué)使用的工具和方式方法等內(nèi)容進(jìn)行了討論;實(shí)驗(yàn)室也得到了艾切曼迪先生、清華大學(xué)劉奮榮教授以及其他邏輯學(xué)界專家的很多幫助.回首國內(nèi)外邏輯教學(xué)軟件的研究成果,國內(nèi)與國外的差距顯著.國外邏輯教學(xué)軟件的開發(fā)和研究己經(jīng)蓬勃興起,內(nèi)容涵蓋廣泛,牽涉?zhèn)鹘y(tǒng)邏輯、數(shù)理邏輯、哲學(xué)邏輯以及其他更深層次的當(dāng)代邏輯分支.阿姆斯特丹大學(xué)、斯坦福大學(xué)、哈fo學(xué)院、哥倫比亞大學(xué)等國際知名學(xué)校在邏輯學(xué)教學(xué)中都已采用了相應(yīng)的邏輯教學(xué)軟件,并獲得了顯著的效果.三、邏輯教學(xué)軟件的實(shí)效性邏輯教學(xué)軟件的實(shí)效性是指在高等院校邏輯學(xué)教育經(jīng)過中,使用邏輯教學(xué)軟件這種當(dāng)代化教育技術(shù)手段的實(shí)際結(jié)果或客觀效果.通常表現(xiàn)為邏輯教學(xué)軟件對(duì)大學(xué)生的影響程度或大學(xué)生接受使用邏輯教學(xué)軟件的邏輯學(xué)教育后的實(shí)際效果.新時(shí)期下,邏輯教學(xué)軟件正以其獨(dú)有的優(yōu)勢逐步深切進(jìn)入到邏輯學(xué)教學(xué)中.邏輯教學(xué)軟件的實(shí)效性主要具體表現(xiàn)出在下面幾個(gè)方面.(一)提高教學(xué)質(zhì)量和教學(xué)效率盡管邏輯學(xué)理論的研究獲得了顯著的成果,但邏輯學(xué)教學(xué)的狀況并不是很樂觀,十分是在我們國家高等教育中.最近幾年來,邏輯通識(shí)教育面臨各種窘境,有關(guān)邏輯學(xué)教學(xué)方面的研究成果很少.邏輯教學(xué)軟件的產(chǎn)生和發(fā)展及其在課堂教學(xué)中的逐步應(yīng)用,促使了邏輯教學(xué)水平的不斷提高.邏輯學(xué)較其他基礎(chǔ)課而言,難學(xué)、難懂、難把握,尤其是當(dāng)代邏輯的內(nèi)容愈加抽象.基于網(wǎng)絡(luò)和計(jì)算機(jī)平臺(tái)的邏輯軟件具有可視化的界面,形象、直觀、生動(dòng)、詳細(xì),而且內(nèi)容豐富,能夠包容大量教學(xué)材料或?qū)嵗?很多繁瑣的、重復(fù)的、形式化的推理演算和驗(yàn)證工作,甚至老師需要評(píng)分的習(xí)題,都能夠交給邏輯軟件來完成,既節(jié)省時(shí)間,又減少錯(cuò)誤,能夠有效地提高教學(xué)質(zhì)量和教學(xué)效率.(二)提高學(xué)生學(xué)習(xí)興趣傳統(tǒng)教學(xué)方式下的邏輯學(xué)教學(xué)經(jīng)過,老師很容易采用灌輸式的理論闡述方式方法教授知識(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é)方式方法,摒棄枯燥的講授法.通過人機(jī)交互式操作,學(xué)生能夠充分發(fā)揮主觀能動(dòng)性,主動(dòng)地探尋求索并獲取自個(gè)所需要的知識(shí),快速把握比擬抽象的邏輯方式方法和規(guī)律,使學(xué)習(xí)變得輕松有趣,大大提高了學(xué)習(xí)興趣.(三)加強(qiáng)大學(xué)生邏輯思維素養(yǎng)作為一門研究人的思維及其規(guī)律的工具學(xué)科,邏輯教育的目的就是為了提高人們的思維能力,提高人們運(yùn)用邏輯工具解決現(xiàn)實(shí)生活中各種問題的能力.隨著當(dāng)代科學(xué)技術(shù)的發(fā)展,以互聯(lián)網(wǎng)、多媒體技術(shù)、數(shù)學(xué)電視、手機(jī)等為代表的新媒體深入地改變著人們的生活方式、思維方式和價(jià)值觀念.邏輯教學(xué)軟件也是當(dāng)代科學(xué)技術(shù)的產(chǎn)物,是邏輯教育的一