李志敏,夏學(xué)文,張學(xué)敏

(孝感學(xué)院計(jì)算機(jī)與信息科學(xué)學(xué)院,湖北孝感432000)

數(shù)理邏輯教學(xué)方法探討

李志敏,夏學(xué)文,張學(xué)敏

(孝感學(xué)院計(jì)算機(jī)與信息科學(xué)學(xué)院,湖北孝感432000)

數(shù)理邏輯不僅是離散數(shù)學(xué)課程的基礎(chǔ),也是計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)其他課程學(xué)習(xí)的重要基礎(chǔ)。文章就如何提高數(shù)理邏輯的教學(xué)質(zhì)量,提出了注重教學(xué)內(nèi)容的合理拓展與延伸、注重?cái)?shù)理邏輯在計(jì)算機(jī)科學(xué)與技術(shù)領(lǐng)域應(yīng)用背景的介紹、注重引入先進(jìn)教學(xué)資源和教學(xué)輔助工具(如ProofWeb)等教學(xué)方法。

離散數(shù)學(xué);數(shù)理邏輯;計(jì)算機(jī)科學(xué)與技術(shù)專業(yè);ProofWeb

離散數(shù)學(xué)是現(xiàn)代數(shù)學(xué)的一個(gè)重要分支,是計(jì)算機(jī)科學(xué)中基礎(chǔ)理論的核心課程。離散數(shù)學(xué)通常研究的領(lǐng)域包括數(shù)理邏輯、集合論、代數(shù)結(jié)構(gòu)、關(guān)系論、函數(shù)論、圖論、組合學(xué)、數(shù)論、形式語(yǔ)言與自動(dòng)機(jī)理論等,它是高校計(jì)算機(jī)及相關(guān)專業(yè)的重要基礎(chǔ)課程之一。學(xué)習(xí)離散數(shù)學(xué),可以培養(yǎng)和提高學(xué)生的抽象思維能力和邏輯推理能力,為學(xué)生繼續(xù)學(xué)習(xí)和工作以及參加科學(xué)研究打下堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)[1]。

數(shù)理邏輯是離散數(shù)學(xué)課程的重要基礎(chǔ),它是用數(shù)學(xué)方法來研究推理的形式結(jié)構(gòu)和推理規(guī)律的數(shù)學(xué)學(xué)科。數(shù)理邏輯的主要分支包括邏輯演算(包括命題演算和謂詞演算)、模型論、證明論、遞歸論和公理化集合論,它與數(shù)學(xué)的其他分支、計(jì)算機(jī)科學(xué)、人工智能、語(yǔ)言學(xué)等學(xué)科均有十分密切的聯(lián)系,并且日益顯示出它的重要作用和更加廣泛的應(yīng)用前景。

近來,各高校非常重視數(shù)理邏輯的教學(xué),例如,復(fù)旦大學(xué)著眼于高起點(diǎn),用泛代數(shù)術(shù)語(yǔ)講授命題邏輯和謂詞邏輯直到完備性、可靠性以及推理,取得優(yōu)良的教學(xué)效果[2]。上海交通大學(xué)用一個(gè)學(xué)期專門講授數(shù)理邏輯,給學(xué)生打下了堅(jiān)實(shí)的理論基礎(chǔ),提高了后續(xù)學(xué)習(xí)能力。

在實(shí)際教學(xué)中,多數(shù)院校數(shù)理邏輯授課時(shí)間僅有20多個(gè)課時(shí),因而教學(xué)內(nèi)容不斷精減,造成學(xué)完這部分知識(shí)后,學(xué)生感覺不能滿足需要。而對(duì)數(shù)理邏輯的把握程度將直接影響到學(xué)生對(duì)后續(xù)專業(yè)課程的學(xué)習(xí),影響到學(xué)生計(jì)算機(jī)思維邏輯的正確形成。提高本科數(shù)理邏輯的教學(xué)水平和質(zhì)量,對(duì)學(xué)生學(xué)習(xí)后面的內(nèi)容具有現(xiàn)實(shí)的意義。本文就如何提高數(shù)理邏輯的教學(xué)質(zhì)量,從三個(gè)方面進(jìn)行了探討。

1 教學(xué)內(nèi)容合理拓展與延伸

1.1 從全面了解數(shù)理邏輯理論體系的角度延伸教學(xué)內(nèi)容

任何邏輯都有兩個(gè)重要層面:語(yǔ)義(semantics)和語(yǔ)法(syntax,也可以稱作是proof theory或proof systems)。研究邏輯一般從語(yǔ)義、語(yǔ)法以及二者之間的聯(lián)系三個(gè)方面展開。由于授課時(shí)間的限制,普通本科生教材通常只介紹語(yǔ)義,較少介紹語(yǔ)法(有的教材叫做形式證明或證明技術(shù)),基本不講語(yǔ)義和語(yǔ)法之間的聯(lián)系。這種處理方式對(duì)少學(xué)時(shí)培養(yǎng)方案而言,不失為是一種選擇。實(shí)踐證明,這種處理顯得較為粗糙,不利于學(xué)生掌握知識(shí)的完整體系和后續(xù)學(xué)習(xí)能力的培養(yǎng)。我們?cè)诮虒W(xué)中需要補(bǔ)充適當(dāng)?shù)慕虒W(xué)內(nèi)容,要讓學(xué)生全面認(rèn)識(shí)數(shù)理邏輯理論的體系[3-4]。為此,我們的做法是在學(xué)完命題邏輯部分后,按以下幾個(gè)層次全面小結(jié)命題邏輯:

1)語(yǔ)法。命題邏輯的形式系統(tǒng)是由命題變?cè)?hào)、邏輯符號(hào)、由這些符號(hào)形成合式公式的規(guī)則、由若干公式組成的公理、由公理經(jīng)一定的法則得到的定理所組成。形式系統(tǒng)的語(yǔ)法就是從公理(或一組公式集)出發(fā)的證明。

2)語(yǔ)義。包括命題的真值、聯(lián)結(jié)詞的意義、命題公式真值、永真式(邏輯等價(jià)式和邏輯蘊(yùn)涵式是永真式的特例)。利用一些基本的邏輯蘊(yùn)涵式、邏輯等價(jià)式以及代入、替換規(guī)則,通過代數(shù)變換,導(dǎo)出更多的邏輯蘊(yùn)涵式、邏輯等價(jià)式,是這一層面的核心內(nèi)容。這部分的教學(xué),要使學(xué)生對(duì)思維的規(guī)律有更清楚的認(rèn)識(shí),對(duì)邏輯的數(shù)學(xué)屬性有更深刻的了解,并能利用代數(shù)變換進(jìn)行語(yǔ)義層面的邏輯推導(dǎo),從一些前提出發(fā),導(dǎo)出它們的邏輯結(jié)果。

3)語(yǔ)義與語(yǔ)法的聯(lián)系。這一部分主要介紹命題邏輯的可靠性定理(命題公式是定理,那么一定是永真式),命題邏輯的形式系統(tǒng)是和諧的(存在公式不是定理),命題邏輯的形式系統(tǒng)的完全性定理和緊致性定理,命題邏輯公式類是可判定的(存在一個(gè)算法判定任一命題公式是否是定理)。

最重要的邏輯是一階邏輯,它是任何邏輯的基礎(chǔ),它的表達(dá)能力很強(qiáng)并且具有良好的性質(zhì)(例如完全性和緊致性)。學(xué)好一階邏輯是進(jìn)一步學(xué)習(xí)的必備基礎(chǔ)。在講授謂詞邏輯時(shí),我們首先引導(dǎo)學(xué)生類比命題邏輯理論體系構(gòu)建謂詞邏輯形式系統(tǒng)的基本理論框架,然后讓學(xué)生利用課外時(shí)間查閱資料,從語(yǔ)義、語(yǔ)法及二者之間的關(guān)系等三方面預(yù)習(xí)課本知識(shí),證明相關(guān)結(jié)論。教學(xué)實(shí)踐證明,上述辦法能較好地提高學(xué)生自主學(xué)習(xí)的積極性。

1.2 從經(jīng)典邏輯到非經(jīng)典邏輯理論的角度拓展教學(xué)內(nèi)容

經(jīng)典邏輯是指由弗雷格、皮爾士、羅素等人創(chuàng)立的現(xiàn)代邏輯系統(tǒng),由統(tǒng)一的命題演算和謂詞演算構(gòu)成,叫做“一階邏輯”,其特點(diǎn)是使用特定的人工符號(hào)語(yǔ)言,運(yùn)用公理化、形式化的方法。經(jīng)典邏輯是研究最深入和使用最廣泛的一類形式邏輯。它們具有如下特征:排中律、無矛盾律、蘊(yùn)涵的單調(diào)性和蘊(yùn)涵的冪等性、合取的交換性、De Morgan對(duì)偶性。

經(jīng)典邏輯的局限性表現(xiàn)在不適合于非直謂性推理、不確定性推理以及內(nèi)涵性推理,特別是經(jīng)典邏輯中存在蘊(yùn)涵怪論和邏輯悖論等無法解決的異?，F(xiàn)象和悖論[5]。

在引入非經(jīng)典邏輯的過程中,要注意講明非經(jīng)典邏輯對(duì)經(jīng)典邏輯的發(fā)展,以及如何克服經(jīng)典邏輯的局限性。

計(jì)算機(jī)科學(xué)與人工智能的需要,促使非經(jīng)典邏輯的理論與應(yīng)用研究持續(xù)發(fā)展。一類非經(jīng)典邏輯是在經(jīng)典邏輯基礎(chǔ)上的拓展。模態(tài)邏輯、時(shí)態(tài)邏輯、道義邏輯等都屬于這一類系統(tǒng)。它們保留經(jīng)典邏輯原有的基本公理、推理規(guī)則和基本算子。例如,模態(tài)邏輯就是在經(jīng)典一階邏輯的基礎(chǔ)上,增加“可能”、“必然”等算子。如果增加“應(yīng)該”、“允許”、“禁止”等算子就稱為道義邏輯,而時(shí)態(tài)邏輯則是增加“過去”、“現(xiàn)在”、“將來”等算子。

另一類非經(jīng)典邏輯是對(duì)經(jīng)典邏輯系統(tǒng)進(jìn)行修改或限制而得到的,如直覺主義邏輯、多值邏輯、模糊邏輯、次協(xié)調(diào)邏輯和相干邏輯等等。這種非經(jīng)典邏輯可以處理經(jīng)典邏輯無法解決的異?，F(xiàn)象。例如,為了邏輯系統(tǒng)解決邏輯系統(tǒng)中的“實(shí)質(zhì)蘊(yùn)涵怪論”,阿克曼創(chuàng)立了相干邏輯。

在引入非經(jīng)典邏輯時(shí),要以學(xué)生現(xiàn)有知識(shí)和容易觀察到的現(xiàn)象為背景。我們?cè)谥v授相干邏輯時(shí),從課本例題出發(fā)。例如命題“如果太陽(yáng)從西邊出來,那么長(zhǎng)江流經(jīng)武漢”,其內(nèi)容上毫不相干,邏輯值卻是真的。對(duì)這樣的蘊(yùn)涵式,引導(dǎo)學(xué)生發(fā)現(xiàn)經(jīng)典邏輯的實(shí)質(zhì)蘊(yùn)涵有弊端。為了避免實(shí)質(zhì)蘊(yùn)涵的弊端,邏輯學(xué)家提出了一條基本原則:蘊(yùn)涵式A→B的前提A和結(jié)論B至少包含一個(gè)共同的變?cè)獣r(shí),公式A→B才是合理的。由此可知,在相干邏輯系統(tǒng)中,如下公式都是無效的:

?P→(p→q),(?pΛp)→q,p→(p→q)

教學(xué)實(shí)踐證明,以教材知識(shí)為基礎(chǔ),適時(shí)將經(jīng)典邏輯進(jìn)行拓展,引入非經(jīng)典邏輯,講清楚非經(jīng)典邏輯的來龍去脈,理清各種邏輯系統(tǒng)的聯(lián)系與區(qū)別,就能幫助學(xué)生理解邏輯系統(tǒng)的構(gòu)造,提高學(xué)生學(xué)習(xí)興趣。

2 數(shù)理邏輯應(yīng)用背景知識(shí)介紹

邏輯的概念、結(jié)論和方法在計(jì)算機(jī)科學(xué)中的地位越來越重要,它是人工智能、程序描述與驗(yàn)證、形式語(yǔ)言、自動(dòng)定理證明和算法理論的重要工具。一般說來,計(jì)算機(jī)科學(xué)中邏輯的作用有兩個(gè)方面:一是服務(wù)于計(jì)算機(jī)科學(xué)研究領(lǐng)域的基礎(chǔ);二是邏輯的語(yǔ)言和演算是軟件開發(fā)、數(shù)據(jù)庫(kù)系統(tǒng)和知識(shí)表示的工具。在這些方面應(yīng)用,已有不少的文章作介紹。我們認(rèn)為數(shù)理邏輯在如下領(lǐng)域的應(yīng)用值得讓本科學(xué)生了解:

1)自動(dòng)定理證明。關(guān)于這一領(lǐng)域,適宜于介紹王浩算法、D-P過程、Robinson歸結(jié)方法。

2)邏輯編程。邏輯編程起源于歸結(jié)證明過程,僅用Horn子句就特別有效。人們發(fā)現(xiàn)Horn子句不僅描述了輸入和輸出關(guān)系,而且還給出了算法,于是產(chǎn)生了使用邏輯作為編程語(yǔ)言的想法。算法重新表達(dá)為:算法=邏輯+控制。

邏輯編程語(yǔ)言是一個(gè)證明程序,即證明系統(tǒng)和搜索策略。邏輯編程中最有意義的一個(gè)問題是:邏輯的哪一部分可以看作是編程語(yǔ)言?

關(guān)于邏輯編程,可以結(jié)合PROLOG講授,讓學(xué)生學(xué)會(huì)使用PROLOG,解決簡(jiǎn)單的應(yīng)用問題。

3)程序驗(yàn)證。程序驗(yàn)證是研究使用形式化方法,嚴(yán)格證明一個(gè)程序符合其預(yù)定目標(biāo),因而是正確無誤的。目前驗(yàn)證還處于初級(jí)階段,近幾十年來,盡管各種各樣的驗(yàn)證工具不斷地被研制出來,但只能作到程序不同程度地被驗(yàn)證。

限于學(xué)生的知識(shí)能力和接受水平,僅簡(jiǎn)單介紹基于邏輯推理的驗(yàn)證。這是說明邏輯在計(jì)算機(jī)科學(xué)中應(yīng)用的有用素材。這種方法將程序驗(yàn)證轉(zhuǎn)換為邏輯推理問題,首先要建立合適的邏輯系統(tǒng),用以描述程序。本科教學(xué)中,介紹最著名的Hoare邏輯,與其他邏輯系統(tǒng)比較,該邏輯系統(tǒng)容易讓學(xué)生接受。

基于Hoare邏輯的程序驗(yàn)證方法的基本思想是對(duì)高級(jí)語(yǔ)言中的每一種基本控制結(jié)構(gòu)(如條件語(yǔ)句、循環(huán)語(yǔ)句)都可以有相應(yīng)的推理規(guī)則,要證明整個(gè)程序的正確性,就是使用這些推理規(guī)則進(jìn)行推導(dǎo)。從理論上講,這種方法非常強(qiáng)大,能證明各種程序的正確性。它的不足之處是要求使用者具有較高的專業(yè)水平,比如能給出循環(huán)不變式。另外,還要求有表達(dá)力非常強(qiáng)的定理證明器,而這些定理證明器目前很難自動(dòng)化。

程序驗(yàn)證的教學(xué)中,不要超過讓學(xué)生了解應(yīng)用邏輯解決實(shí)際問題的方法這個(gè)層次,主要目的還是激發(fā)學(xué)生學(xué)習(xí)的興趣。

3 基于ProofWeb的數(shù)理邏輯教學(xué)系統(tǒng)

數(shù)理邏輯的教學(xué),離不開網(wǎng)絡(luò)資源的輔助。在此我們介紹基于ProofWeb的數(shù)理邏輯教學(xué)系統(tǒng),它是由Cezary Kaliszyk和Freek Wiedijk等人于2006年開發(fā)完成的“計(jì)算機(jī)輔助邏輯教學(xué)系統(tǒng)”[6]。

數(shù)理邏輯是計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)本科以及研究生階段的基礎(chǔ)課程。它的兩個(gè)最基本,也是最重要的組成部分是“命題演算”和“謂詞演算”。在數(shù)理邏輯的學(xué)習(xí)過程中,練習(xí)是關(guān)鍵的活動(dòng)之一,常常出現(xiàn)一些學(xué)生不能判斷近似正確但并不是完全正確的證明,雖然學(xué)生也可以使用一些計(jì)算機(jī)程序,引導(dǎo)他們發(fā)現(xiàn)完全正確的證明,而這樣做的一個(gè)缺點(diǎn)是學(xué)生可能會(huì)偶然得到解題方法,但并不真正理解證明過程。實(shí)踐證明將傳統(tǒng)方式和計(jì)算機(jī)程序引導(dǎo)相結(jié)合的方式是最好的選擇。

3.1 ProofWeb系統(tǒng)簡(jiǎn)介

ProofWeb系統(tǒng)具有如下兩個(gè)優(yōu)勢(shì):

第一,該系統(tǒng)必須通過一個(gè)網(wǎng)絡(luò)界面,使學(xué)生在中央服務(wù)器上進(jìn)行學(xué)習(xí)過程,證明助手不在學(xué)生的電腦上運(yùn)行,而是在服務(wù)器上運(yùn)行。這種架構(gòu)的第一個(gè)好處是學(xué)生不需要安裝任何軟件,他們可以從任何電腦經(jīng)過互聯(lián)網(wǎng)連接使用,不受地域和時(shí)間的限制;第二個(gè)好處是學(xué)生不需要考慮軟件的版本問題,由于一切都是在同一個(gè)中央服務(wù)器上,學(xué)生們?cè)谌魏螘r(shí)間可以得到軟件的授權(quán)版本,練習(xí)題目及其可能解答,老師也可以在任何時(shí)候知道學(xué)生的學(xué)習(xí)狀況。

第二,該系統(tǒng)充分利用了最先進(jìn)的證明助手,即Coq。該系統(tǒng)成功驗(yàn)證了著名的四色定理和C語(yǔ)言編譯器等數(shù)學(xué)和計(jì)算機(jī)科學(xué)相關(guān)理論和應(yīng)用課題。

Cezary Kaliszyk和Freek Wiedijk等人開發(fā)的ProofWeb系統(tǒng)增加了如下功能模塊:

1)備有大量的邏輯練習(xí)題,設(shè)置的難度級(jí)別涵蓋了非常容易到非常難,學(xué)生不會(huì)很快就可以完成全部練習(xí)。

2)課程介紹和使用說明書,系統(tǒng)提出的證明與教科書同步,系統(tǒng)開發(fā)了Gentzen-型和Fitch-型兩個(gè)自然演繹變種。

ProofWeb系統(tǒng)突出的特點(diǎn)是該系統(tǒng)使用嚴(yán)謹(jǐn)?shù)淖C明助手和基于Web應(yīng)用程序架構(gòu),學(xué)生學(xué)習(xí)情況保留在Web服務(wù)器上,學(xué)生本人、老師和系統(tǒng)可以隨時(shí)了解學(xué)生學(xué)習(xí)進(jìn)展。

3.2 ProofWeb使用方法介紹

ProofWeb系統(tǒng)既能用于邏輯教學(xué)又能作為證明助手。ProofWeb用戶有3種登陸方式:第一,不需要注冊(cè)登錄;第二,如果是學(xué)習(xí)邏輯或證明助手課程的學(xué)生,系統(tǒng)提供免費(fèi)課程,如果是教師用戶,并希望在此服務(wù)器上進(jìn)行教學(xué),可發(fā)送郵件至proofweb@cs.ru.nl聯(lián)系;第三,教師還可以下載ProofWeb系統(tǒng)并在自己的服務(wù)器上運(yùn)行。

具體操作步驟如下:

1)進(jìn)入網(wǎng)頁(yè)http://prover.cs.ru.nl/,注意ProofWeb不一定在所有的瀏覽器上運(yùn)行正常,在Firefox上一般沒問題。

2)在靠近頁(yè)面的底部點(diǎn)擊課程名稱。

3)輸入用戶名和密碼。

4)按一下你想工作的問題的按鈕。

5)可以選擇Debug菜單上的項(xiàng)目Toggle E-lectric Terminator,這樣每輸入一個(gè)‘.’時(shí),命令自動(dòng)執(zhí)行,否則將需要按向下箭頭或輸入controldown執(zhí)行命令。

6)點(diǎn)擊向下箭頭或輸入control-down,直到已經(jīng)執(zhí)行了定理行后面的證明行。現(xiàn)在,開始進(jìn)行證明工作。這時(shí),不完整版本的證明會(huì)顯示在右下角。

7)用下一頁(yè)描述的一系列策略取代(＊!prop_proof＊)的注釋。如果您沒有做第5步的Toggle Electric Terminator,那么需要反復(fù)按向下箭頭(或輸入control-down)執(zhí)行證明策略。

8)用戶也可以從模板、向后和向前的菜單選擇輸入策略項(xiàng)目,用標(biāo)簽、公式和項(xiàng)取代問號(hào)(‘?’),這樣做之后,按一下向下箭頭或輸入control-down。

9)用戶可以修改尚未被處理的部分文字(已被處理部分將變成綠色),若要撤消證明步驟,點(diǎn)擊向上箭頭或輸入control-up。

10)如果用戶有關(guān)于ProofWeb的問題,或交流經(jīng)驗(yàn),可以使用ProofWeb形式的課程討論板。

應(yīng)用ProofWeb系統(tǒng)進(jìn)行教學(xué),可以培養(yǎng)學(xué)生自主學(xué)習(xí)能力,減少教師批閱學(xué)生證明練習(xí)的時(shí)間。成功開發(fā)系統(tǒng)ProofWeb,也是數(shù)理邏輯的一個(gè)典型應(yīng)用案例。

4 結(jié)束語(yǔ)

本文針對(duì)數(shù)理邏輯教學(xué)中存在的問題,提出了一些教學(xué)建議,經(jīng)在孝感學(xué)院計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)離散數(shù)學(xué)課程教學(xué)實(shí)踐中運(yùn)用,效果較好,主要表現(xiàn)在學(xué)生學(xué)習(xí)興趣不斷增強(qiáng),提高了學(xué)生自主學(xué)習(xí)能力,培養(yǎng)了研究型學(xué)習(xí)習(xí)慣。

[1] 屈婉玲,耿素云,張立昂,等.離散數(shù)學(xué)[M].北京:高等教育出版社,2008.

[2] 朱洪.離散數(shù)學(xué)教程[M].上海:上?？茖W(xué)技術(shù)文獻(xiàn)出版社,1996.

[3] 王元元.計(jì)算機(jī)科學(xué)中的現(xiàn)代邏輯學(xué)[M].北京:科學(xué)出版社,2002.

[4] 王元元,陳衛(wèi)衛(wèi),賀汛.離散數(shù)學(xué)數(shù)理邏輯教學(xué)中值得關(guān)注的幾個(gè)問題[J].計(jì)算機(jī)教育,2009(16):136-138.

[5] 王輝.邏輯理論變革的必然趨勢(shì)[J].遼寧工學(xué)院學(xué)報(bào),2003,5(2):36-37.

[6] Cezary Kaliszyk,Freek Wiedijk.Teaching logic using a state-of-the-art proof assistant[C]//Proceedings of PATE’07.Elsevier,2007.

Abstract:Mathematical logic is a foundation of discrete mathematics and also an important basic knowledge for learning in computer science and technology speciality.In this paper,for the purpose of improving teaching quality of mathematical logic,the authors proposed teaching approach from the aspects of focusing on the reasonable extending of teaching content,introducing applications-oriented background knowledge and the advanced teaching resources and aided teaching tools such as Proof-Web.

Key Words:discrete mathematics;mathematical logic;computer science and technology speciality;ProofWeb

On the Teaching Approach of Mathematical Logic

Li Zhimin,Xia Xuewen,Zhang Xuemin
(School of Computer and Inf ormation Science,Xiaogan University,Xiaogan,Hubei432000,China)

G642.41

A

1671-2544(2010)03-0105-04

2010-04-06

李志敏(1967— ),男,湖北云夢(mèng)人,孝感學(xué)院計(jì)算機(jī)與信息科學(xué)學(xué)院講師,博士。

(責(zé)任編輯:張曉軍)