數理邏輯教學方法探討

李志敏,夏學文,張學敏

(孝感學院計算機與信息科學學院,湖北孝感432000)

數理邏輯教學方法探討

李志敏,夏學文,張學敏

(孝感學院計算機與信息科學學院,湖北孝感432000)

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

離散數學;數理邏輯;計算機科學與技術專業(yè);ProofWeb

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

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

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

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

1 教學內容合理拓展與延伸

1.1 從全面了解數理邏輯理論體系的角度延伸教學內容

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

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

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

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

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

1.2 從經典邏輯到非經典邏輯理論的角度拓展教學內容

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

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

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

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

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

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

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

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

2 數理邏輯應用背景知識介紹

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

1)自動定理證明。關于這一領域,適宜于介紹王浩算法、D-P過程、Robinson歸結方法。

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

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

關于邏輯編程,可以結合PROLOG講授,讓學生學會使用PROLOG,解決簡單的應用問題。

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

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

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

程序驗證的教學中,不要超過讓學生了解應用邏輯解決實際問題的方法這個層次,主要目的還是激發(fā)學生學習的興趣。

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

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

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

3.1 ProofWeb系統(tǒng)簡介

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

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

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

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

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

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

ProofWeb系統(tǒng)突出的特點是該系統(tǒng)使用嚴謹的證明助手和基于Web應用程序架構,學生學習情況保留在Web服務器上,學生本人、老師和系統(tǒng)可以隨時了解學生學習進展。

3.2 ProofWeb使用方法介紹

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

具體操作步驟如下:

1)進入網頁http://prover.cs.ru.nl/,注意ProofWeb不一定在所有的瀏覽器上運行正常,在Firefox上一般沒問題。

2)在靠近頁面的底部點擊課程名稱。

3)輸入用戶名和密碼。

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

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

6)點擊向下箭頭或輸入control-down,直到已經執(zhí)行了定理行后面的證明行?，F在,開始進行證明工作。這時,不完整版本的證明會顯示在右下角。

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

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

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

10)如果用戶有關于ProofWeb的問題,或交流經驗,可以使用ProofWeb形式的課程討論板。

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

4 結束語

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

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

[2] 朱洪.離散數學教程[M].上海:上海科學技術文獻出版社,1996.

[3] 王元元.計算機科學中的現代邏輯學[M].北京:科學出版社,2002.

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

[5] 王輝.邏輯理論變革的必然趨勢[J].遼寧工學院學報,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— ),男,湖北云夢人,孝感學院計算機與信息科學學院講師,博士。

(責任編輯:張曉軍)