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. Si-mon) 等人首先取得突破,他们编制的模拟人的启发式搜索问题解决的计算机程序"逻辑理论家"证明了罗素和怀德海合着的《数学原理》第二章中的38 条逻辑推理.后来经过改进,又证明了该章的全部 52 条逻辑推理.此后,世界着名逻辑学家美籍华人王浩教授在 IBM-704 计算机上以 3 ~ 5 分钟的时间证明了《数学原理》中有关命题演算的全部 220 条逻辑推理,并且还证明了该书中带等词的谓词演算的 150 条逻辑推理的 85%.不久,他仅用 8. 4 分钟的时间证明了以上全部逻辑推理[3].同一时期,我国着名数学家吴文俊教授也在自动定理证明方面做出了突出的贡献,他提出的把几何问题代数化的方法被国际上的学者称为"吴方法".随着计算机科学技术的迅速发展,自动推理的作用显得越来越重要,许多逻辑学家尝试使用计算机来模拟逻辑的思想和方法,从而研发了一系列的逻辑软件,推动了逻辑学教育技术的现代化.现代信息技术带来了现代化的教学手段,也对传统的教学方式和教学手段进行了革新.
同多媒体课件、电子学习资源、网络课程等现代化的教育技术手段一样,逻辑教学软件在逻辑教学过程也发挥着十分重要的作用.
进入 21 世纪,逻辑软件的开发及在逻辑教学中的应用逐渐成为逻辑教育过程中极为重要的一个环节.2000 年、2006 年和 2011 年,在西班牙的萨拉曼卡大学,分别召开了 3 次关于"逻辑教学工具"的国际性学术研讨会.这 3 次会议将逻辑教学软件的开发和使用作为重要议题来讨论,对逻辑软件的发展前景、逻辑教学软件在逻辑教学中的作用等具体问题进行了深入的研究,引起了逻辑学界对逻辑教学软件的广泛兴趣和重视,有力地推动了逻辑教学软件的发展.
二、逻辑教学软件的研究状况
从操作模式来看,逻辑软件主要有计算机网络在线逻辑软件和计算机程序设计逻辑软件两类.计算机网络在线逻辑软件是基于万维网的,有逻辑教学网络平台的支持,并由软件供应商提供程序在线服务.在线逻辑软件有对应的网络链接,学习者直接在网络界面下使用,可以进行互动练习,操作简便.计算机程序设计逻辑软件是用某种程序设计语言编写,运行于 Windows 或 Mac等操作系统上的应用软件.程序设计逻辑软件由用户安装在计算机中,执行特定的功能,操作具有独立性.根据形式逻辑的分类,逻辑软件也可分为传统逻辑软件、数理逻辑软件、哲学逻辑软件等等.
( 一) 国外逻辑教学软件的研究
国外对逻辑软件的研发已经取得了丰富的成果.早在 1980 年,美国斯坦福大学语言与信息研究中心( CSLI) 就研发了一系列具有开创性和实效性的逻辑应用软件,用于本科生数理逻辑课程的教学和研究.目前,在国外的大学逻辑学教学中,较多地使用了逻辑软件,特别是一些现代逻辑软件的应用已经相当地成熟和完善.
我们参考国外的逻辑教育网站,简要介绍一些流行且实用的逻辑软件.
1. 亚里士多德词项逻辑( Computational Aristo-telian Term Logic)①亚里士多德词项逻辑是由德国逻辑学家克劳斯·格拉斯霍夫( Klaus Glashoff) 于 2004 年开发的一款传统逻辑软件.这款逻辑在线软件的主要功能是学习亚里士多德三段论逻辑的自然演绎系统.该软件预设了全部的三段论演绎规则,输入三段论的前提,并选择相应的有效论式,执行后就可以直接得到结论.
2. 逻辑工具箱( Logic Toolbox)②逻辑工具箱是约翰·萨埃蒂( John Saetti) 于2009 年开发的一个在线教学平台.其中的范畴逻辑计算器( Categorical Logic) 也是一款关于三段论学习的传统逻辑软件.该软件对传统逻辑性质判断中的主项和谓项之间的外延关系,用构造出的文恩图做出判断和检验,还可以进行直言推理、三段论推理、连锁推理和省略式三段论推理.
3. 树证明发生器( Tree Proof Generater)③树证 明 发 生 器 是 由 沃 尔 夫 冈 ( WolfgangSchwarz) 于 2007 年 11 月发布的一个利用 JavaS-cript 程序设计的在线逻辑软件.树证明的方法也称作语义表,是检查各种逻辑公式有效性的一种有效算法.这款数理逻辑软件为经典的命题逻辑和不含等词的谓词逻辑提供语义表.用户只需输入要验证的、有效的命题公式或谓词公式,系统就会自动生成一棵证明树或者给出反模型的证明.
4. 逻辑 动 画 入 门 ( Introductory Logic Anima-tions)④1988-1999 年,由荷兰阿姆斯特丹大学的贾恩( Jan Jaspars) 等人开发的逻辑动画入门也是利用 JavaScript 程序设计的一个在线逻辑软件.该软件可以对基础数理逻辑和哲学逻辑的形式演算进行互动训练,包括命题逻辑、谓词逻辑、模态逻辑、动态逻辑和图灵机 5 个功能模块,每一个功能模块又由若干子程序组成.例如,命题逻辑功能模块下的子程序: 命题计算器( propositional calcu-lator) 可判定一个命题逻辑公式是否是重言式、矛盾式或可满足式,以及该公式真值为真或假时,其命题变项的真值组合.谓词逻辑功能模块下的子程序: 谓词计算器( predicate calculator) 用来计算给定模型上的谓词逻辑公式的结果,并查找自由变项的正反实例.模态逻辑功能模块的子程序:
可能世界计算器( possible world calculator) 可在一个给定的克里普克( Kripke) 模型中计算出哪些世界能够验证输入的模态公式.动态逻辑功能模块下的子程序: 传递计算器( transition calculator) 可以计算一个给定正则表达式的传递外延.
5. 交 互 式 逻 辑 程 序 ( Interactive Logic Pro-grams)⑤交互式逻辑程序是加拿大滑铁卢大学的斯坦利·贝尔雷斯( Stanley N. Burris) 开发的在线教学平台,包括真值表 ( Truth Tables) 、命题联结词( Propositional Connectives) 、戴维斯 - 帕特南程序( Davis-Putnam procedure) 、合一算法( UnificationAlgorithm) 、自动定理证明器 ( Automated TheoremProver) 等一系列逻辑软件.例如,命题联结词程序可令用户选择任意的常项 0、1,否定词"﹁"和16 进制的二元联结词,然后验证哪些联结词可以由已选定的联结词得到.戴维斯 - 帕特南程序允许用户最多选择 10 个子句,然后后台运用戴维斯- 帕特南方法确定所选子句集是否是可满足的.合一算法程序允许用户选择两个前缀形式的项,然后找出它们的一致置换,等等.
6. 柏拉图( Plato)⑥柏拉图是美国得克萨斯大学的罗伯特·昆斯( Robert C. Koons) 开发的逻辑在线教学平台,用于形式逻辑基础课程的学习,内容包括在线课程、软件下载、学习指南、专业词典等.柏拉图程序能够使用户构造命题演算和谓词演算形式语言中的证明,也可用来构造包括集合论部分在内的形式化的数学证明.
7. 通向逻辑之门( Gateway to Logic)⑦奥地利维也纳大学的克里斯汀·戈特沙尔( Christian Gottschall) 开发的通向逻辑之门在线平台集一些基于网络的逻辑程序为一体,并提供了一些逻辑函数,如真值表、范式、证明检验、证明构造等.服务器端函数( Server-side Functions) 用来计算经典二值命题逻辑的公式,由真值表、重言式检验、图解表达式树、文本表达式树、合取范式、典范合取范式、析取范式、典范析取范式等一系列函数组成.证明生成器( Proof Builder) 是能够交互式地构造证明的程序.证明检查器( Proof Check-er) 可以检验用户提交的证明.自动定理证明器( Automated Theorem Prover) 适用于经典的谓词逻辑,可以自动地推出有效论证,直接在服务器端上执行.
8. 阿卡网络平台( Akka flies the Web)①荷兰阿姆斯特丹大学的莱克斯 ( Lex Hen-driks) 于 1998 年开发的阿卡网络平台可以检验一些逻辑系统中公式的可证明性和模型中公式的有效性,为动态逻辑绘制并编辑克里普克模型,以及用计算机测定逻辑语义图.阿卡是对克里普克模型进行定理测试和模型测试的工具,提供克里普克模型编辑器并且支持模型测试,还可提供附加的服务,如语义图的构造.
此外,瑞士伯尔尼大学开发的逻辑工作台( The Logics Workbench) ,②美国德克萨斯州农业机械大学开发的逻辑后台程序和课堂测验( LogicDaemon and Quizmaster) ,③美国犹他大学开发的表达式计算器( Expression Evaluator)④等等,都是用于形式逻辑学习的在线逻辑教学平台.
9. 语言、证明和逻辑( Language,Proof and Log-ic)语言、证明和逻辑教学软件包,简称 LPL,是美国斯坦福大学语言与信息研究中心( CSLI) 研发的一套专门用于一阶逻辑语言学习的计算机程序组件.该教学软件包与美国逻辑学家、印第安那大学的巴威斯( Jon Barwise) 及其在斯坦福大学语言与信息研究中心的同事艾克曼迪 ( JohnEtchemendy) 合着的 《一阶逻辑的语言》,以及他们二人合着的改进版本《语言、证明和逻辑》二书配套使用[4].LPL 软件包是目前最为成熟、功能上更加完善的一组数理逻辑学习软件,包括布尔( Boole) 、费奇( Fitch) 、塔斯基的世界( Tarski'sWorld) 3 个逻辑程序和一个基于互联网的分等级服务: 提交( Submit) .这些程序能在计算机操作系统 Windows 或 Mac 下使用.
布尔程序用于构造逻辑公式的真值表.其最大的特点就是对公式中所含命题变项的个数没有限制并能同时构造若干个命题的真值表.塔斯基的世界程序用于学习一阶语言及其语义.用户可以在该程序设计的三维空间里使用和改造已有的世界或创造新的世界,编写一阶逻辑的语句,判断它们的真值,还可以通过做游戏,检验自己对语句真值的判断是否正确,从而掌握逻辑联结词和量词的用法.费奇程序用于构造自然推理系统 F 下的形式证明.用户可以运用相应的推理规则分步骤验证一阶公式的形式证明.提交程序用于网上提交作业.学生的作业可以直接递交给评分服务器( Grade Grinder) ,它将给作业评分并将结果发送给学生及导师.
10. 超证明( Hyperproof)超证明也是由巴威斯和艾克曼迪共同研发的一款用于分析谓词逻辑自然演绎形式的推理过程的程序软件.这款程序仅适用于苹果机型,与二人 1994 出版的《超证明》一书配套使用.超证明是分析推论和证明过程的规则的一个学习系统,与传统的对一阶逻辑处理的方式不同,它包含图形信息和句子信息,综合不同的信息形式,描述出一系列的推理规则.这种方式能够使学生集中于证明内容的信息,而不是句子的语法结构,从而利用一种直观的证明系统,学会构建后承和非后承的证明,将标准的句法规则扩展为用图形表示的合并信息.超证明软件能够检查每一证明类型的逻辑有效性,适用于各种自然演绎形式的证明系统,包括巴威斯和艾克曼迪的一阶逻辑语言的系统.还适用于塔斯基的世界程序,能构造和检查塔斯基的世界语言中的证明.它允许用户将图形表示的信息和图形相适合的演绎技术、句子和语法规则组合,对塔斯基的世界中的块世界进行推理,使得学习一阶逻辑具有极大的乐趣.
11. 超求解器( Hypersolver)超求解器是由土尔其比尔肯大学的阿克曼( V. Akman) 和土尔其海峡大学的帕克坎( M. Pak-kan) 于 1993 年研发的一款利用解引理在非良基集合全域中解方程的程序软件.非良基集合( Non-well-founded sets) ,也称超集( Hypersets) ,是具有循环性质或无穷∈降链性质的集合.1987年,美国着名逻辑学家巴威斯( J. Barwise) 和艾切曼迪( J. Etchemendy) 为了证明非良基集合的存在性,引入解引理说明每个方程组有唯一解,即把集合看作方程组的解.为了得到更为丰富的集合全域,保证非良基集合的存在,以便对各种循环现象做出解释,可以在标准集合论中用非良基公理替换良基公理,从而得到非良基集合论.而非良基集合论给出了一套完备的工具能够刻画现实世界中各种各样的循环问题.就此而言,非良基集合论的作用和影响已经远远超出了经典的集合论 ZFC[5].
解引理是非良基集合论的特色.超求解程序,是一个基于解引理的、独立操作的程序,可以对根据集合定义的方程组进行求解.它具有内置的图解功能,能够显示出描述用户输入方程以及这些方程解的图.超求解器的用户接口,称作命令接口.用户输入有效的一个文件,文件中的每一行都是一个方程,文件被送到语法解析器转变为 Lisp( 列表处理语言) 形式,并检验是否符合输入要求.之后,超求解器的解算器将解引理应用到所输入的方程组,进行求解.接下来是图显示部件的调用,这一部件输入解算器产生的方程组的解,最后由图绘制程序描述出方程组的解决方案图并显示在图显示窗中.
除了具有数学上的重要性和精确性之外,超求解器还提供了刻画各种循环现象的一种有趣的方法.在人工智能领域中,信息能够以方程组的形式来安排,因而该程序是进行常识推理的一个非常有用的实用工具.超求解程序具有一般的语法分析器和直观的图形界面,也是数理逻辑的重要工具程序之一.超求解程序的实施,使得利用解引理模型化循环的现象同计算机自动化求解问题紧密地结合起来,极具应用价值[6].
( 二) 国内逻辑教学软件的研究
国内对逻辑教学软件的研究相对国外而言还十分薄弱,刚刚进入起步阶段.2007 年 5 月,南开大学哲学院建设了国内第一个"逻辑推理"实验室,也是目前国内高校中唯一的一个用于逻辑学学科教学的实验平台.该实验室具有多媒体网络功能,配备有苹果 iMac、激光打印机、投影机等硬件设备和 LPL、超证明等一些逻辑教学软件,主要用于逻辑学专业本科生和研究生数理逻辑课程的实验教学.实验室的建立,改善了逻辑学学科的教学条件,在该学科领域的教学中引入现代化技术,逐渐与国际逻辑学教学接轨.
近几年来,实验室负责人李娜教授及成员在数理逻辑课程的教学过程中,将逻辑软件同逻辑学教科书、教学课件一样作为教学工具来使用.
实验室使用的逻辑软件主要是从国外购买的教学软件包,以及国外的网络在线教学软件.此外,实验室还开发了两个教学软件,一个是能够快速构造真值表、计算命题公式真值的逻辑软件: 逻辑运算 3. 0.①这款软件有中英两个版本,适用于 Win-dows 操作平台,能够计算不超过 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 forcommonsense set Theory[G]/ / Gün L,?nvural R,Ge-lenbe E,et al. Proceedings of Eight International Sympo-sium on Computer and Information Sciences. Turkey: Is-tanbul,1993: 436 - 443.
