吳方法在離散數學謂詞演算教學中的應用

摘要:離散數學是現代科學的一個重要分支,是計算機科學中基礎理論的核心課程,而謂詞邏輯是其中一個十分重要的內容之一。如何將計算機自動推理的另一個經典方法——吳方法引入到離散數學的教學中是本文著重探討的問題。

關鍵詞:離散數學;自動推理;吳方法

中圖分類號:O158文獻標識碼:A文章編號:1007-9599 (2010) 06-0000-00

Application of Wu"s Method in Predicate Calculus Discrete Mathematics Teaching

Li Yi

(University of Electronic Science and Technology,National Computer Experiment Teaching Center,Chengdu610054,China)

Abstract:Discrete Mathematics is an important branch of modern science,is the basic theory of computer science core curriculum,and predicate logic is one of the important contents.How to Computer Automated Reasoning another classic method - Wu introduced into the teaching of discrete mathematics is the focus of this issue.

Keywords:Discrete mathematics;Automated reasoning;Wu"s method

一、引言離散數學是計算機科學與技術專業的一門核心課程

作為數學的一個分支,其研究的對象是各種各樣的離散量的結構及其離散量之間的關系。通過這門課程的學習,可以培養學生們嚴密的數學思維能力。同時,離散數學與計算機科學中的數據結構、操作系統、編譯理論、數字邏輯理論、算法分析、邏輯程序設計、系統結構、容錯診斷、機器定理證明、計算機網絡、人工智能等課程有著緊密的聯系。

離散數學的基礎知識主要包括數理邏輯、集合論、抽象代數、格、布爾代數以及圖論。對于工科學生,教學中,不僅要從數學的邏輯性和嚴密性上去論述所涉及的數學理論知識,更要注重培養學生了解這些數學知識在計算機科學諸領域中所起的應用作用。數理邏輯往往是工科學生在學習離散課程中最早接觸的內容,且與人工智能和定理機器證明有著極大的聯系。因此,如何讓學生學好數理邏輯將直接關系到學生邏輯推理能力提高。謂詞演算的演繹推理是數理邏輯部分的重點和難點內容,里面涉及到大量的知識點。教學實踐表明,工科學生對這部分的內容往往難以掌握。而大部分院校在講授謂詞演算推理時,往往采用“紙和筆”的形式向學生演示整個推理的過程,甚少采用人機交互的方式。

本文中,針對謂詞演算的演繹和推理,我們探討了如何將吳方法引入到該教學內容中,以此從側面來幫助學生了解數學推理的本質,加深他們對計算機自動推理的認識,提高學習數理邏輯的熱情。

二、謂詞演算的演繹和推理

在謂詞邏輯中,為了研究命題內的內在聯系就必須對命題做進一步的分解。

例1:小王是老師

對上述命題進行分解得到:首先,這里的“小王”被稱為個體;“是老師”被稱為謂詞。如果用字每s來表示小王,用字母Q來表示謂詞“是學生”。那么,上述命題可表為Q(s)。當需要描述個體間的關系時,就要引入二元謂詞。

例2:10小于3

引進謂詞Q,則上述命題可表位Q(10,3)。

此外,為了更好地刻畫命題函數所表達的意思,往往還需要引進量詞: 。在引入了個體、謂詞和量詞之后,謂詞邏輯的表達就更加廣泛了。如:

例3:并非所有的實數都是有理數

引進謂詞R和Q,有 。

命題演算系統是被包含在謂詞演算系統之中。因此,在謂詞演算系統內,除了要使用命題演算系統所使用的RP,RT和CP規則外,還要引入關于量詞的4條重要性質的推理規則:

US(全稱特指規則):

ES(存在特指規則):

UG(全稱推廣規則):

EG(存在推廣規則):

應用上述4條規則以及命題演算的推理規則,使得謂詞演算公式的推理過程可類似于命題演算中推理理論那樣進行。這樣的推理方法常常需要一些技巧,在教學過程也很少通過計算機向學生演算整個推理過程。為了加深學生對計算機自動推理的理解,并便于人機交互的形式去演示推理過程,我們將計算機代數中的經典推理方法——吳方法引入到謂詞演算推理的教學中。不同于前面介紹的經典邏輯推理,吳方法的引入實現了幾何、代數命題推理的機械化。

三、幾何定理機器證明

定理的機器證明是自動推理和符號計算領域最為活躍的分支之一。我國數學家吳文俊在70年代末提出的吳方法是在計算機上證明和發現幾何定理,解決各種幾何問題的有效工具。定理機器證明的思想可追溯到17世紀的G.W.Leibniz和R.Descartes。它的目標是要把一類數學問題當作一個整體,建立一種統一的,確定的證明過程,使得該類的定理只要按程序步驟機械地進行下去,在有限步后,就一定能判斷出定理的真偽。這方面的工作可分為:以Hebrand理論及歸結原理為代表的邏輯方法;以A.Newll及H.A.Simon等人的工作為代表的人工智能方法;以Tarski理論和吳方法為代表的代數方法。吳方法從提出至今,已在世界各國廣泛傳播,并出現了大量的學術論著。吳方法的發現使初等幾何真正跨入了機械化階段。當人們在初等幾何范圍內提出新命題而不知真假時,只要上機一試,便知分曉。而人的工作則主要是猜測、發現,并從機器證明的定理中挑選最漂亮的加以分析。吳方法的基本思想非常樸素:把幾何命題化為代數形式加以處理。

例4:設梯形ABCD的兩條對角線之中點的連線EF與梯形的一邊AB相交,那么直線EF將線段AB平分(如圖)。

當然,對此例,可以使用謂詞邏輯的推理方法進行推斷定理的真偽。這種推理方法需要一些技巧才能完成,且推理過程在教學中不便于通過計算機采用人機交互方式進行演示。因此,我們采用吳方法來進行自動推理,使得整個推理過程可通過計算機實時演示,從而使教學過程可視化。根據吳方法,

第一步,選取Descartes坐標系,不失一般性,將各點坐標依次選為:

于是,定理的假設由下列關系構成:

E是AC中點

F是BD中點

M是AB和EF交點

要證明的結論是:

M是AB中點

至此,我們已經完成了吳方法證明定理的第一步:用解析幾何方法將問題代數化。剩下的問題就是,在假設一組多項式為0的條件下,求證另一組多項式為0。對本例,這就是:

設 求證

第二步,吳-ritt整序原理。將 或 中的變元 消去,得到一個導元為 的多項式,再用 將該多項式中的 消去,繼而將 或 中的 消去。最后得到 的特征列為

其中, 。

第三步,偽除。即對 ,都有 。這說明,在非退化條件 下,定理是成立的。事實上,這些非退化條件是有幾何意義的:

AD不與BC重合;

AB不與AD垂直;

ABCD不是平行四邊形。

從上述過程易見,吳方法將推理的過程轉變為代數方程組整相關的問題。

四、推理平臺Maple

上述的三個步驟完全可以在計算機上通過人機交互的方式進行計算推理。這里,我們主要采用計算機代數系統Maple進行上述推理計算。

Maple是1980年由加拿大waterloo大學開發出來的。

當初開發Maple的目的是為了解決繁雜的代數運算問題。如今其版本已提升到Maple13,并已發展成一個相當完備的軟件。它提供的數學元算工具相當完備,氣符號運算能力使我們能一步一步地進行復雜的公式推導。對例4中的推理,我們僅需要將 對應的表達式鍵入到Maple工作區中;然后,調用Maple函數 計算 的值是否均為0。若是,則定理為真;否則,定理為假。此方法雖然是代數的,但它提供了一個可視化的方式去引導學生對計算機推理的認識。同時,通過在課堂上比較邏輯推理和吳法代數推理之間的差異和各自的特點,加深學生對謂詞演算推理方式的理解。

五、結束語

由于謂詞演算的推理涉及到大量規則的使用,因此在利用相關規則推理時,需要一定的技巧性。在教學方法上,針對工科學生的特點,我們不僅要注重啟發創新,引入新方法,使教學內容豐富多彩,而且還要培養學生們的嚴密的邏輯思維能力。具體體現在,教學中,多采用可視化強,可人機交互的方式進行授課,從而便于學生容易理解和接受。對大部分概念都用實例加以說明;強化基本概念的描述,注重基本理論的證明方法。此外,對同一個問題,引導學生采用多種方法進行求解,充分發揮學生的主觀能動性。通過開設實驗課,使學生們不僅要掌握書上的理論知識,還要讓他們了解這些知識的應用背景,真正做到學以致用。

參考文獻:

[1]傅彥.離散數學基礎及應用[M].電子科技大學出版社,2000.8

[2]左孝凌,李為鑑,劉永才.離散數學[M].上?？茖W技術文獻出版社,1982,9

[3]魏長華,王光明,魏媛媛. 離散數學及其應用[M].武漢大學出版社,2006.6

[4]楊路,張景中,侯曉榮. 非線性代數方程組與定理機器證明[M].上?？萍?a href="http://www.trylelo.com/k/jiaoyu/" target="_blank" class="keylink">教育出版社,1995,12

[5]吳文俊.幾何定理機器證明的基本原理[M].科學出版社,1984

[6]何鋒.離散數學教學中的命題符號化難點討論[J].計算機教育,2007,(9):38-40

[7]師雪霖,尤楓,顏可慶.離散數學教學聯系計算機實踐的探索[J].計算機教育.2008,(20):113-115

[8]劉光潔.談談離散數學的教學[J].計算機教育,2007,(12):62-64

[9]藺永政,王新紅,李金屏.“離散數學”中實踐教學的探討[J].計算機教育,2006,(10):103-104

作者簡介:李軼,男,博士,主要研究方向為:符號計算、程序驗證。