3. 數(shù)學(xué)定理的計(jì)算機(jī)證明
數(shù)學(xué)定理的
計(jì)算機(jī)證明,又稱
機(jī)器證明,有廣義和狹義之說。
廣義之說是,數(shù)學(xué)定理的機(jī)器證明,顧名思義,就是通過機(jī)器的有限步推斷完成一般數(shù)學(xué)定理的證明,簡(jiǎn)稱為
機(jī)器證明,又稱為
機(jī)械化證明、
自動(dòng)證明,因計(jì)算機(jī)是實(shí)現(xiàn)這類證明的最好機(jī)器,甚至也可以說是現(xiàn)在唯一真正可用的機(jī)器,所以常稱為
計(jì)算機(jī)證明;
狹義之說是,把數(shù)學(xué)的某一類命題(數(shù)量可很多)從整體上加以考慮,建立統(tǒng)一的、確定的證明程序,經(jīng)計(jì)算機(jī)有限步推斷給出數(shù)學(xué)命題真假的證明,真者就成為定理。
從廣義上講,如四色定理、費(fèi)馬大定理等在計(jì)算機(jī)上進(jìn)行的證明,應(yīng)屬于數(shù)學(xué)定理計(jì)算機(jī)證明的;但這類證明,一事一例,獨(dú)具特點(diǎn),不是對(duì)一類數(shù)學(xué)定理的證明,因此,從狹義上講,它們并不屬于數(shù)學(xué)定理的計(jì)算機(jī)證明。
數(shù)學(xué)定理的計(jì)算機(jī)證明是現(xiàn)代數(shù)學(xué)中一個(gè)新興的邊緣性學(xué)科,也是現(xiàn)代人工智能發(fā)展的一個(gè)重要方向,以下均簡(jiǎn)稱為機(jī)器證明或計(jì)算機(jī)證明。從傳統(tǒng)的定理手工證明到定理計(jì)算機(jī)證明,是現(xiàn)代數(shù)學(xué)思想方法的一次重大突破,既是計(jì)算機(jī)和人工智能發(fā)展的產(chǎn)物,也是數(shù)學(xué)自身發(fā)展的需要。
4. 計(jì)算機(jī)證明的可行性
西方的幾何學(xué)是由歐幾里德建立的一套公理化系統(tǒng)發(fā)展起來的,是按照定義——公理——定理——證明的演繹系統(tǒng)進(jìn)行的。顯然,這種公理化體系的幾何定理證明現(xiàn)在還很難實(shí)現(xiàn)機(jī)械化。由于幾何在數(shù)學(xué)中的歷史地位及在數(shù)學(xué)教育中的重要作用,對(duì)幾何定理進(jìn)行計(jì)算機(jī)證明成了這一領(lǐng)域中的研究重點(diǎn)。
如何利用機(jī)器進(jìn)行自動(dòng)推理,特別是進(jìn)行幾何定理的自動(dòng)證明,是西方學(xué)術(shù)界長(zhǎng)期以來試圖研究解決的問題。事實(shí)上,17世紀(jì)大數(shù)學(xué)家萊布尼茲就有機(jī)械化證明的設(shè)想;直到19世紀(jì)末,由于希爾伯特(David Hilbert)及其追隨者建立并發(fā)展了數(shù)理邏輯,這一問題才有了明確的數(shù)學(xué)形式;又由于20世紀(jì)40年代計(jì)算機(jī)的出現(xiàn),才使這一設(shè)想有了實(shí)現(xiàn)的可能和條件。
歷史上一些大師級(jí)的數(shù)學(xué)家,曾在幾何定理計(jì)算機(jī)證明這條路上進(jìn)行過艱苦的探索。
為了用統(tǒng)一的方法處理千變?nèi)f化的幾何問題,笛卡爾(Ren Descartes)發(fā)明了坐標(biāo)方法,創(chuàng)立了解析幾何。跨19世紀(jì)、20世紀(jì)的大數(shù)學(xué)家希爾伯特,在它的名著《幾何基礎(chǔ)》中,曾給出了一類幾何問題的機(jī)械化解題方法。電子計(jì)算機(jī)的出現(xiàn),大大加快了數(shù)學(xué)定理計(jì)算機(jī)證明研究的進(jìn)程,促進(jìn)了幾何問題求解的計(jì)算機(jī)證明研究。
1948年,塔斯基(Alfred Tarski)發(fā)表了一條引人注目的定理:“
一切初等幾何和初等代數(shù)命題構(gòu)成的命題類,是可判定的”。這里,所謂“
命題”是一個(gè)具有前提和結(jié)論的判斷句;如果命題的前提和結(jié)論都可以用有限個(gè)整系數(shù)多項(xiàng)式的等式或不等式表達(dá),就叫做初等幾何和初等代數(shù)命題。如果有一套機(jī)械的方法,對(duì)于某個(gè)命題類的任一個(gè)命題,都能用這套方法經(jīng)有限步的操作確定命題的真假,就說這個(gè)命題類是“
可判定的”。
波蘭裔猶太邏輯學(xué)家、數(shù)學(xué)家、語言哲學(xué)家阿 塔斯基 (1901–1983)
塔斯基的方法,先利用笛卡爾坐標(biāo)把幾何問題化為代數(shù)問題,再用代數(shù)方法來解決問題。沿這條路線,發(fā)展了幾何問題計(jì)算機(jī)證明的代數(shù)方法。
1975年,考林斯(Collins)提出“柱面代數(shù)分解方法”,比塔斯基的方法效率提高了很多,但在計(jì)算機(jī)上仍只能解決個(gè)別稍有難點(diǎn)的幾何問題。
笛卡爾——塔斯基——考林斯,這是用代數(shù)方法尋求幾何問題機(jī)械求解的一條線。
另一條路線,是企圖把解決幾何問題的傳統(tǒng)綜合方法機(jī)械化,通常叫做后推搜索法,又提出了更有效的前推搜索法。這類方法,由于搜索空間過大等問題,未能形成有效的算法。
計(jì)算機(jī)早期只會(huì)進(jìn)行單一的數(shù)值計(jì)算,到了20世紀(jì)60年代中,用它能做符號(hào)計(jì)算,有理式的四則運(yùn)算,多項(xiàng)式的因式分解,求最小公倍式和最大公因式,甚至還能計(jì)算符號(hào)微積分,為幾何問題的計(jì)算機(jī)證明提供了強(qiáng)有力的工具。
1977年,我國(guó)著名數(shù)學(xué)家吳文俊院士在《中國(guó)科學(xué)》雜志上發(fā)表了論文“初等幾何判定問題與機(jī)械化證明”,提出了一個(gè)證明等式型初等幾何定理的新的代數(shù)方法。1984年,中國(guó)留美學(xué)者周咸青在他的博士論文中把這個(gè)方法叫做
“吳方法”,并列出了基于吳方法所編寫的程序證明的130個(gè)幾何定理。不久,他又在一本專著中列出了用吳方法證明的512個(gè)幾何定理。吳方法從此在國(guó)際自動(dòng)推理研究領(lǐng)域廣為傳播。
1984年,吳文俊院士的學(xué)術(shù)專著《幾何定理計(jì)算機(jī)證明的基本原理(初等幾何部分)》出版。這本專著遵循機(jī)械化思想引進(jìn)數(shù)系和公理,依照機(jī)械化觀點(diǎn)系統(tǒng)地分析了各類幾何體系,諸如帕斯卡幾何(Pascal's theorem),垂直幾何,度量幾何,歐氏幾何等,證明確立了各類幾何的機(jī)械化定理,系統(tǒng)地闡明了幾何定理機(jī)械化證明代數(shù)方法的基本原理。
《幾何定理機(jī)器證明的基本原理》一書
1992年,張景中院士和周咸青博士合作研究,提出了以面積法為工具,用計(jì)算機(jī)生成幾何定理“短證明”的設(shè)想。這項(xiàng)工作被自動(dòng)推理領(lǐng)域的國(guó)際同行譽(yù)為“計(jì)算機(jī)發(fā)展幾何問題解題能力道路上的里程碑”,“自動(dòng)推理領(lǐng)域30年來最重要的工作”。
1993年,張景中、楊路、高小山和周咸青等人把消點(diǎn)法推廣到了非歐幾何,用計(jì)算機(jī)發(fā)現(xiàn)了幾十條非歐幾何的新定理,并且自動(dòng)生成了它們的可讀證明。
迄今,人們已經(jīng)用計(jì)算機(jī)證明了上百條重要的數(shù)學(xué)定理,甚至還曾經(jīng)用計(jì)算機(jī)發(fā)現(xiàn)過一些猜想。
5. 計(jì)算機(jī)證明的應(yīng)用
目前,計(jì)算機(jī)證明作為數(shù)學(xué)研究的一種方法,還存在著許多理論和技術(shù)上的問題,這些問題的解決將有待于算法理論、計(jì)算機(jī)科學(xué)和人工智能等各個(gè)領(lǐng)域出現(xiàn)新的重大突破。
近30多年來,數(shù)學(xué)定理計(jì)算機(jī)證明的研究從基礎(chǔ)研究領(lǐng)域擴(kuò)展到了應(yīng)用研究和開發(fā)研究領(lǐng)域。這里所說的應(yīng)用既有間接的,也有直接的。
在研究幾何定理計(jì)算機(jī)證明時(shí),創(chuàng)造或發(fā)展了一些新的方法或代數(shù)工具,它們可以用來解決其他領(lǐng)域的問題,如機(jī)構(gòu)設(shè)計(jì)、曲面造型、計(jì)算機(jī)輔助設(shè)計(jì)、機(jī)器人控制、計(jì)算機(jī)視覺以及其他有關(guān)的數(shù)學(xué)問題,這是間接應(yīng)用。
把幾何定理機(jī)器求解的程序發(fā)展為軟件,或者嵌入計(jì)算機(jī)應(yīng)用軟件,這是直接的應(yīng)用。這類應(yīng)用的實(shí)際需求,主要有兩個(gè)方面:一是為研究者、教師和數(shù)學(xué)愛好者提供智能性幾何解題電子詞典,對(duì)兩千多年的初等幾何作一個(gè)相對(duì)完美的總結(jié);二是應(yīng)用幾何定理機(jī)器求解研究的成果,可以研制出高智能的教育軟件。
通過計(jì)算機(jī)證明,解決了數(shù)學(xué)中的百年難題,如四色猜想、費(fèi)馬大定理等,開闊了人類的視野,為數(shù)學(xué)發(fā)展開辟了一條新途徑,意義重大,也是計(jì)算機(jī)證明的又一直接應(yīng)用。
計(jì)算機(jī)證明同樣有導(dǎo)致發(fā)現(xiàn)的功能,其中一個(gè)較為典型的例子是分形幾何的創(chuàng)立。早在20世紀(jì)20年代,法國(guó)數(shù)學(xué)家朱利亞(Gaston Julia)就開始著手研究分形幾何,但是由于這種幾何圖形的驚人復(fù)雜性,朱利亞的研究沉寂了幾十年。直到60年代以后,美國(guó)數(shù)學(xué)家曼德勃羅 ( B.Mandelbrot )開始用計(jì)算機(jī)來畫圖,才使分形幾何得到了真正的發(fā)展。
分形幾何圖形一例
社會(huì)的需求還會(huì)把機(jī)器求解的研究推向更廣的領(lǐng)域,不僅研究幾何問題的機(jī)器求解,而且要探討一般理科問題的機(jī)器求解方法。