數(shù)學機械化的思想_第1頁
數(shù)學機械化的思想_第2頁
數(shù)學機械化的思想_第3頁
數(shù)學機械化的思想_第4頁
數(shù)學機械化的思想_第5頁
已閱讀5頁,還剩31頁未讀, 繼續(xù)免費閱讀

下載本文檔

版權說明:本文檔由用戶提供并上傳,收益歸屬內容提供方,若內容存在侵權,請進行舉報或認領

文檔簡介

從吳文俊和吳方法談起一

數(shù)學機械化的思想數(shù)學文化課程組

1中國科學院院士第三世界科學院院士首屆國家最高科技獎國家第一屆自然科學獎

最高獎一等獎自動推理的最高獎

Herbrand

獎2006邵逸夫數(shù)學獎吳文俊2中央電視臺《大家》欄目:《吳文俊

·我的不等式》片斷3什么是數(shù)學機械化所謂機械化,無非是刻板化和規(guī)格化。

數(shù)學

問題的機械化,就要求在運算或證明過程中,

每前進一步之后,都有一個確定的、必須選

擇的下一步,這樣沿著一條有規(guī)律的、刻板

的道路,

一直達到結論。使用一種機械化方法證明一類定理,才真正

體現(xiàn)了機械化定理證明。1977年,吳文俊給

出了初等幾何一類主要定理的機械化證明方法一“吳方法”。4數(shù)學機械化

從設想到實現(xiàn)希爾伯特萊布尼茨笛卡爾5數(shù)學機械化:從設想到實現(xiàn)吳文俊哥德爾塔斯基王浩6笛卡爾的設想17世紀法國的數(shù)學家

Descartes

曾有過一個偉大

的設想:

“一切問題化為數(shù)學問題,

一切數(shù)學問題

化為代數(shù)問題,

一切代數(shù)問題化為代數(shù)方程求解問

題。"Descartes

把問題想得太簡單了,如果他的設想真

能實現(xiàn),那就不僅是數(shù)學的機械化,而是全部科學

的機械化。因為代數(shù)方程求解是可以機械化的。但

Descartes

沒有停留在空想,他所創(chuàng)立的解析

幾何,在空間形式和數(shù)量關系之間架起了一座橋梁,實現(xiàn)了初等幾何問題的代數(shù)化。7萊布尼茲之夢德國數(shù)學家

Leibniz

曾有過“推理機器”的設想。他研究過邏輯,設計并制造出能做乘法的計算機,進而萌發(fā)了設計萬能語言和造

一臺通用機器的構想。他的努力促進了

Boole

代數(shù)、數(shù)理邏輯以及計算機科學的研究,正是沿著這一方向,經(jīng)后人的努力,形成了機器定理證明的邏輯方法。8希爾伯特的構想Hilbert在

《幾何基礎》中提出了從公理化走向機械

化的數(shù)學構想。

Hilbert

計劃將數(shù)學知識納入嚴格的

公理體系中,并著力在公理化基礎上尋找機械化的

方法判定命題是否成立。

Hilbert

同時指出,定理的

判定問題應當是分類解決的,解決方法要同時強調

簡單性和嚴格性。在

Hilbert

的名著《幾何基礎》

一書中就提供了一

條可以對一類幾何命題進行判定的定理一當然,在那個時代,不僅

Hilbert

本人,整個數(shù)學界都沒

有意識到這一點。9哥德爾的著名結果G?del

著名的不完全性定理指出一個不弱于初等數(shù)論的形式系統(tǒng)如果是無矛盾的,則是

不完全的

,即存在形式系統(tǒng)的一個命題,它

和它的否定都不能由形式系統(tǒng)證明。因此,

Hilbert

的要求太高了。上述的Godel不完全性定理斷言:即使在初等數(shù)論的范圍

內,對所有命題進行判定的機械化方法也是

不存在的!10塔斯基的判定法波蘭數(shù)學家

Tarski

1950

年推廣了關于代

數(shù)方程實根數(shù)目的

Sturm

法則,由此證明了

一個引人注目的定理:

“一切初等幾何和初

等代數(shù)范圍的命題,都可以用機械方法判定。"Tarski

得出的結論給定理證明機械化的研究帶來了曙光??上姆椒ㄌ珡碗s,即使用

高速計算機也證明不了稍難的幾何定理。11王浩:邁向數(shù)學機械化1959

年,王浩設計了一個程序,用計算機證

明了

Russell

、

Whitehead

的巨著《數(shù)學

原理》中的幾百條有關命題邏輯的定理,僅

用了9分鐘。

王浩工作的意義在于宣告了用

計算機進行定理證明的可能性。在1960年的《IBM

研究與發(fā)展年報》

(IBMJournal),

王浩發(fā)表了《邁向數(shù)學機械化》(Toward

Mechanical

Mathemat

ics

),

“數(shù)學機械化”一詞即出自此處。12吳文?。簷C器證明領域的新的一頁1977

年,吳文俊在《中國科學》上發(fā)表論文《初等幾何判定問題與機械化問題》。

1984

年,吳文

俊的學術專著《幾何定理機器證明的基本原理》由

科學出版社出版,這部專著著重闡明幾何定理機械

化證明的基本原理。

1985

年,吳文俊的論文《關

于代數(shù)方程組的零點》發(fā)表,具體討論了多項式方

程組所確定的零點集。與國際上流行的代數(shù)理想論

不同,明確提出了具有中國自己特色的、以多項式

零點集為基本點的機械化方法。自此,

“吳方法”

宣告誕生,數(shù)學機械化研究揭開了新的一幕。13對吳方法的評價吳方法遵循中國傳統(tǒng)數(shù)學中幾何代數(shù)化的思想,與通?;?/p>

數(shù)理邏輯的方法根本不同,

首次實現(xiàn)了高效的幾何定理自動

證明,顯現(xiàn)了無比的優(yōu)越性。他的工作被稱為自動推理領域

的先驅性工作,并于1997年獲得

“Herbrand

自動推理杰出

成就獎"。在授獎辭中對他的工作給了這樣的介紹與評價:"幾何定理自動證明首先由赫伯特"格蘭特(HerbertGerlenter)于50年代開始研究。雖然得到一些有意義的結果,

但在吳方法出現(xiàn)之前的20

年里,這一領域進展甚微。在不多

的自動推理領域中,這種被動局面是由一個人完全扭轉的。

吳文俊很明顯是這樣一個人。他將幾何定理證明從一個不太

成功的領域變?yōu)樽畛晒Φ念I域之一?!?4數(shù)學機械化得到國際數(shù)學界承認2006年,著名數(shù)學家吳文俊榮獲邵逸

夫數(shù)學科學獎。邵逸夫數(shù)學科學獎是一項國際性大獎,它的評委是來自國際數(shù)學界

的知名權威。吳文俊說:這次邵逸夫獎的評委都是國際上有影響的大家,他們宣布我獲得邵逸夫獎,是因為我的數(shù)學機械化

問題的研究,這實際上是國際數(shù)學界對數(shù)

學機械化研究的承認與肯定,它比獎金重要得多。15《吳文俊

·我的不等式》片斷16三角形三條高線交于一點的代數(shù)證明D是BC

和CA

上高線交點B(x?,0)A(x?,O)0(0,0)17定理的假設部分是AD

⊥BC

?x?x?-x?(x?-x?)=0BD

⊥AC

?x?x?-x?(x?-x?)=0由吳方法,可得非退化條件是

x?

(x?-x?)≠0定理的結論是CO

經(jīng)過D

?

x?=0顯然在非退化條件下定理成立。18任意三角形中,

一個角的三等分線,與和

它相鄰的角的三等分線相交,交點組成正

三角形。Morley定理19機器方法容易證明Morley定理任意三角形中,

一個角的三等分線,與和

它相鄰的角的三等分線相交,按一定的規(guī)

則選取交點,共可組成27個三角形,在這

27個三角形中,

一定有18個是正三角形。用機器方法容易證明這個更一般的Morley

定理。在證明過程中,多次出現(xiàn)關于12個

變量的含有一千多項的多項式。20定理的假設相當于一組

多項式方程定理的結論相當于一個

多項式方程上面的諸F

稱為假設多

項式,

G

稱為終結多項

式。F?=0,..,Fs=0G=0吳方法概要21吳方法概要(續(xù))吳方法是給出了一個機械化方法,在有限步內給出一組非退化條件多項式D1,.,D,又根據(jù)這一機械化方法足以在有限步內,判定在

非退化條件D?≠0,..,D,≠0下,

G=0是否可從F?=0,.,Fs=0

推出。22C(u?,u?)E(x?,x?)B(u1,0)平行四邊形對角線互相平分D(x?,2?)A(0,0)23題設和結論表成代數(shù)形式AD//BC:u?(u?-u?)-xu?=0E

在BD

上:

x?

(x?-u?)-u?

(x?-u?)=0E

在AC

上:x?U?-x?U?=0結論EA=EC:u2-2u?x?+u3-2u?x?=024吳方法的處理題設部分三角化,得到三個多項式:f?=u?-u?-xf?=x?(x?-u?-u?)+uu?f?=x?U?-x?U?再把結論左邊的多項式除以f3,所得的余式除以左,所得的余式除以f,

看最后所得的余式是不是恒等于

零。25中國古代數(shù)學的貢獻70年代初,吳文俊開始研讀中國數(shù)學史。1975年,他撰寫了《中國古代數(shù)學對世界文化的偉大

貢獻》,文中詳細列舉在代數(shù)、幾何、三角、解

析幾何和微積分等學科的發(fā)現(xiàn)和創(chuàng)立過程中,中

國傳統(tǒng)數(shù)學所起的重大作用。吳文俊指出,

中國傳統(tǒng)數(shù)學注意解方程,在代數(shù)學、幾何學、極限概念等方面既有豐碩的成果,

又有系統(tǒng)的理論。26中國古代數(shù)學的特色中國傳統(tǒng)數(shù)學強調構造性和算法化,注意解決科學實驗

和生產(chǎn)實踐中提出的各類問題,往往把所得到的結論以

各種原理的形式予以表述。在中國古代,求兩數(shù)最大公約數(shù)即等數(shù)用更相減損之術。

如求24與15的等數(shù),其逐步減損如下:(24,15)→

(9,15)→

(9,6)→

(3,6)→

(3,3)其理由不證自明。中國傳統(tǒng)數(shù)學在從問題出發(fā)以解決問題為主旨的發(fā)展過

程中建立了以構造性與機械化為其特色的算法體系,《九章算術》與劉徽的《九章算術注》是這一機械化體

系的代表作,這與西方數(shù)學以歐幾里得《幾何原本》為

代表的所謂公理化演繹體系正好遙遙相對。27機械化思想是中國古代數(shù)學的精髓吳文俊把中國傳統(tǒng)數(shù)學的思想概括為機械

化思想,指出它是貫穿于中國古代數(shù)學的

精髓。他列舉大量事實說明,中國傳統(tǒng)數(shù)

學的機械化思想為近代數(shù)學的建立和發(fā)展做出了不可磨滅的貢獻。這種機械化思想,不僅曾深刻影響了數(shù)學

的歷史進程,而且對數(shù)學的現(xiàn)狀也正在發(fā)

揚它日益顯著的影響。28數(shù)

學機械化的廣泛應用吳文俊特別重視數(shù)學機械化方法的應用,明確提出“數(shù)學機械化方法的成功應用,是數(shù)學機械化

研究的生命線"

。他不斷開拓新的應用領域,如

控制論、曲面拼接問題、機構設計、化學平衡問

題、平面天體運行的中心構形等,還建立了解決全局優(yōu)化問題的新方法。吳方法還被用于若干高科技領域,得到一系列國際領先的成果,包括曲面造型、機器人結構的位

置分析、智能計算機輔助設計(CAD)

、信息傳輸

中的圖像壓縮等。29從開普勒定律到牛頓定律開普勒定律為(1)行星繞太陽以橢圓軌道運行,太陽為一焦點(2)太陽到行星的向量在相同的時間掃過相同的

面積牛頓定律為(3)行星的加速度與太陽到行星的距離的平方成

反比利用吳方法在微分域上的推廣,可以從開普勒經(jīng)驗公式自動推導出牛頓定律。30機器人與連桿機構的運動分析如圖,綠色的平臺是活動平臺,下面的平臺是固定的,

六根連桿長度可變,求連桿長度變化時平臺上一點的 軌跡。31機器人與連桿機構的運動分析已知連桿機構的構成,求該機構上某一點的軌跡

及該點的位置與連桿機構的關系,這類問題稱為

機械設計中的正解問題。前面的例子就是一個正

解問題。反過來,求解連桿機構的參數(shù)使得連桿機構上一

點恰好位于空間指定位置的問題稱為機械設計中

的逆解問題。這兩類問題都可以看成方程求解問題。吳文俊用特征集方法解決了一般PUMA型機器人的逆解問題,研究了四連桿的設計問題。

32在幾何設計中,有一大類問題要確定一給定次數(shù)的代數(shù)曲面按一定要求連接已給的若干代數(shù)曲面。這類問題可以用吳方法解決。左圖是一個連接三根管道的例子。曲面連接問題33腦力勞動的機械化在新的正在到來的工業(yè)革命中,可以認為是以某

種設備代替人腦。這將使人類艱苦思考的價值為

之降低,

是一種腦力勞動的機械化。這種機械化由于上世紀中葉計算機的發(fā)明而有某種可能。數(shù)學是一種典型的腦力勞動。由于數(shù)學思維具有

其它思維方式所沒有的簡潔、明確、嚴密、清晰

等優(yōu)點,因而數(shù)學的機

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內容里面會有圖紙預覽,若沒有圖紙預覽就沒有圖紙。
  • 4. 未經(jīng)權益所有人同意不得將文件中的內容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內容的表現(xiàn)方式做保護處理,對用戶上傳分享的文檔內容本身不做任何修改或編輯,并不能對任何下載內容負責。
  • 6. 下載文件中如有侵權或不適當內容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準確性、安全性和完整性, 同時也不承擔用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

評論

0/150

提交評論