數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件

如何實現(xiàn)自動推理--簡明介紹數(shù)學機械化與吳方法講座2008-11-？朝魯上海海事大學數(shù)學系如何實現(xiàn)自動推理講座2008-11-？朝魯上海講座一、吳文俊簡介講座一、吳文俊簡介

吳文俊院士是中國科學院數(shù)學與系統(tǒng)科學研究院的研究員，我國著名的數(shù)學家。他于上世紀50年代對數(shù)學的主要領域—拓撲學做出了杰出貢獻。70年代后期，吳文俊開創(chuàng)了嶄新的數(shù)學機械化領域。他建立了用計算機證明幾何定理的“吳方法”。實現(xiàn)了高效幾何定理自動證明；吳方法應用于計算機圖形學、機器人、機構設計、全局優(yōu)化、化學平衡、天體運行……等領域。87歲≠不能創(chuàng)新

吳文俊院士獲得過很多獎項：1956年獲得國家自然科學一等獎1979年獲得中國科學院自然科學一等獎1990年獲得第三世界科學院數(shù)學獎1993年獲得陳嘉庚數(shù)理科學獎1994年獲得首屆香港求是科技基金會杰出科學家獎1998年度國際自動推理界的最高獎“Herbrand獎”

2000年獲得首屆國家最高科技獎2006年獲邵逸夫數(shù)學科學獎87歲≠不能創(chuàng)新吳文俊院士獲得過很多獎項：/detail2.asp?project_id=122&type_id=22看一段視頻報道/detail2吳文俊的虛擬軸機床——數(shù)學機械化方法及其在并聯(lián)機構中的應用

吳文俊院士開創(chuàng)了數(shù)學機械化研究領域。他所建立的“吳方法”，“吳消元法”及“吳有限核定理”已成為該領域的奠基性成果。運用數(shù)學機械化方法，本項研究解決了廣義Stewart平臺正解問題，這是對機器人運動學領域的一個主要貢獻。以此為基礎，研制成功我國第一臺大型虛擬軸機床樣機與集成電路制造裝備關鍵子系統(tǒng)。吳文俊的虛擬軸機床——數(shù)學機械化方法及其在并聯(lián)機構中的應用數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件二、腦力勞動能機械化嗎？二、腦力勞動能機械化嗎？勞動=體力勞動+腦力勞動;

17世紀以來，工業(yè)革命使人們逐漸實現(xiàn)了體力勞動的機械化，大大地促進了社會生產力的發(fā)展。?!勞動=體力勞動+腦力勞動;17世紀以來，工業(yè)革命使人們逐漸

腦力勞動的徹底機械化是不可能，但部分機械化是完全可能，并且隨著人類智慧的提高這個機械化程度越來越高。意義深遠!腦力勞動的機械化是人類的追求,夢想腦力勞動的徹底機械化是不可能，但部分機械化是完全可能，并且

作為科學基礎的數(shù)學研究是典型的腦力勞動，具有論證嚴謹、表述明確等優(yōu)點，理應率先實現(xiàn)機械化。成為其他學科機械化的基礎。如今，人類社會正步入信息革命時代,計算機的功能不斷增強，為人類實現(xiàn)腦力勞動的機械化創(chuàng)造了物質條件。對腦力勞動的機械化，作為其靈魂或核心技術,數(shù)學的參與是不可缺少。作為科學基礎的數(shù)學研究是典型的腦力勞動，具有論證三、數(shù)學機械化

與自動推理三、數(shù)學機械化

吳文?。核^機械化，無非是刻板化和規(guī)格化。數(shù)學問題的機械化，就要求在運算或證明過程中，每前進一步之后，都有一個確定的、必須選擇的下一步，這樣沿著一條有規(guī)律的、刻板的道路，一直達到結論。數(shù)學機械化吳文?。核^機械化，無非是刻板化和規(guī)格化。數(shù)學機械自動推理機械化算法的計算機實現(xiàn)。對某一個思維問題(腦力勞動)要設計機械化算法;算法是構造化的,能轉化為計算機指令;計算機能接受并能按設計邏輯處理這些指令,推理出結論.這里要知道兩個關鍵點:計算機能處理什么?算法是構造性(機械化)?自動推理機械化算法的計算機實現(xiàn)。實現(xiàn)機械化和自動推理需要兩個發(fā)展：

構造性數(shù)學的發(fā)展（腦子）；計算機的發(fā)展（肢體）。出現(xiàn)了“數(shù)學機械化”、“自動推理”、“計算機代數(shù)”,“理論計算機”，……等學科。實現(xiàn)機械化和自動推理需要兩個發(fā)展：出現(xiàn)了“數(shù)學機四、數(shù)學機械化的艱難歷程

——從設想到實現(xiàn)四、數(shù)學機械化的艱難歷程數(shù)學機械化：從設想到實現(xiàn)笛卡爾萊布尼茨希爾伯特數(shù)學機械化：從設想到實現(xiàn)笛卡爾萊布尼茨希爾伯特數(shù)學機械化：從設想到實現(xiàn)哥德爾塔斯基王浩吳文俊數(shù)學機械化：從設想到實現(xiàn)哥德爾塔斯基王浩吳文俊笛卡爾的設想

17

世紀法國的數(shù)學家Descartes曾有過一個偉大的設想：“一切問題化為數(shù)學問題，一切數(shù)學問題化為代數(shù)問題，一切代數(shù)問題化為代數(shù)方程求解問題。”

并，Descartes

沒有停留在空想，他所創(chuàng)立的解析幾何，在空間形式和數(shù)量關系之間架起了一座橋梁，實現(xiàn)了初等幾何問題的代數(shù)化。但，Descartes把問題想得太簡單了，如果他的設想真能實現(xiàn)，那就不僅是數(shù)學的機械化，而是全部科學的機械化。笛卡爾的設想萊布尼茲之夢德國數(shù)學家Leibniz

曾有過“推理機器”的設想。他研究過邏輯，設計并制造出能做乘法的計算機，進而萌發(fā)了設計萬能語言和造一臺通用機器的構想。他認為,他的方案一旦實現(xiàn),人們之間的一切爭論都可以被心平氣和的機器體力勞動所代替。他的努力促進了Boole代數(shù)、數(shù)理邏輯以及計算機科學的研究，正是沿著這一方向，經后人的努力，形成了機器定理證明的邏輯方法。

萊布尼茲之夢德國數(shù)學家Leibniz曾有過“推理機器”的希爾伯特的構想

Hilbert在《幾何基礎》中提出了從公理化走向機械化的數(shù)學構想。Hilbert計劃將數(shù)學知識納入嚴格的公理體系中，并著力在公理化基礎上尋找機械化的方法判定命題是否成立。Hilbert同時指出，定理的判定問題應當是分類解決的，解決方法要同時強調簡單性和嚴格性。在Hilbert

的名著《幾何基礎》一書中就提供了一條可以對一類幾何命題進行機械化判定的定理—當然，在那個時代，不僅Hilbert

本人，整個數(shù)學界都沒有意識到這一點。

希爾伯特的構想Hilbert在《幾何基礎》哥德爾的著名結果

G?del著名的不完全性定理指出一個不弱于初等數(shù)論的形式系統(tǒng)如果是無矛盾的，則是不完全的，即存在形式系統(tǒng)的一個命題，它和它的否定都不能由形式系統(tǒng)證明。因此，Hilbert的要求太高了。上述的G?del不完全性定理斷言：即使在初等數(shù)論的范圍內，對所有命題進行判定的機械化方法也是不存在的！哥德爾的著名結果G?del著名的不完全性定理塔斯基的判定法

波蘭數(shù)學家Tarski

在1950年推廣了關于代數(shù)方程實根數(shù)目的Sturm法則，由此證明了一個引人注目的定理：“一切初等幾何和初等代數(shù)范圍的命題，都可以用機械方法判定?！?/p>

Tarski得出的結論給定理證明機械化的研究帶來了曙光?？上姆椒ㄌ珡碗s，即使用高速計算機也證明不了稍難的幾何定理。

塔斯基的判定法波蘭數(shù)學家Tarski在1950王浩：邁向數(shù)學機械化1959年，王浩設計了一個程序，用計算機證明了Russell、Whitehead的巨著《數(shù)學原理》中的幾百條有關命題邏輯的定理，僅用了9分鐘。王浩工作的意義在于宣告了用計算機進行定理證明的可能性。在1960年的《IBM研究與發(fā)展年報》（IBMJournal）上，王浩發(fā)表了《邁向數(shù)學機械化》（TowardMechanicalMathematics）的文章。“數(shù)學機械化”一詞即出自此處。王浩：邁向數(shù)學機械化1959年，王浩設計了一個程序，

其他人與王浩同一時期，A.Newell和H.A.Simon也做了與王浩類似的工作。1965年Robinson歸結原理的提出是用邏輯方法進行機器證明的又一重要進展。1976年K.I.Appel和W.Haken在高速電子計算機上用1200小時的計算時間，證明了著名的四色定理，使數(shù)學家們100多年來未能解決的這個難題得到了肯定的回答（機械化證明）。數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件數(shù)學大師們的堅持不懈地追求,表明數(shù)學機械化思想重要而深刻。但數(shù)學機械化歷程漫長而艱難，發(fā)展緩慢。70年代末，在中國得到突破！數(shù)學大師們的堅持不懈地追求,表明數(shù)學機械化思想重要而深刻。

五、數(shù)學機械化的突破

——吳方法的出現(xiàn)五、數(shù)學機械化的突破吳文?。?/p>

數(shù)學機械化（機器證明）領域的新的一頁

1976年，我國數(shù)學家吳文俊教授為數(shù)學機械化（機器證明，自動推理）的發(fā)展翻開了新的一頁。提出幾何定理的機器證明機械化算法，并計算機實現(xiàn)。他當時既沒有接觸到Tarski的工作,也沒有想到Hilbert的著作里那一條定理。中國古代構造性數(shù)學思想的啟迪了他。吳文俊：

數(shù)學機械化（機器證明）領域的新的一頁1971977年，吳文俊在《中國科學》上發(fā)表論文《初等幾何判定問題與機械化問題》。1984年，吳文俊的學術專著《幾何定理機器證明的基本原理》由科學出版社出版，這部專著著重闡明幾何定理機械化證明的基本原理。1985年，吳文俊的論文《關于代數(shù)方程組的零點》發(fā)表，具體討論了多項式方程組所確定的零點集。與國際上流行的代數(shù)理想論不同，明確提出了具有中國自己特色的、以多項式零點集為基本點的機械化方法。自此，“吳方法”宣告誕生，數(shù)學機械化研究揭開了新的一幕。

1977年，吳文俊在《中國科學》上發(fā)表論文《初等幾何判定問

六、吳方法的介紹六、吳方法的介紹

所謂定理的機械化證明，就是對一類定理（這類定理可能成千上萬）提供一種統(tǒng)一的方法，使得該類定理中每個定理，都可依此方法給出證明。在證明過程中，每前進一步，都有章可循地確定下一步該做什么和如何做。

從“一理一證”到“－類一證”，是數(shù)學的認識和實踐的飛躍。數(shù)學(腦力勞動)機械化的典范所謂定理的機械化證明，就是對一類定理（這類吳方法的基本思想是十分樸素的:把幾何命題化成代數(shù)形式加以處理?；墒裁葱问?如何處理?整個過程是什么樣?主要思想是什么?吳方法的基本思想是十分樸素的:

Simson定理的機器證明

Simson定理：在的外接圓上任取一點P。自P點向直線BC,CA,AB引垂線,垂足依次為R,S,T，那么R,S,T三點在一直線上(如圖所示)。O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:R,S,T共線。用一個例子來簡單介紹吳方法Simson定理的機器證明Simson定理：在

為了簡便，可以將△ABC的外接圓中心O取為Descartes坐標原點，將圓半徑取為單位長，并設各點的坐標為

A(x1,y1)，B(x2,y2)，C(x3,y3)，R(x4,y4)，S(x5,y5)，T(x6,y6)，P(1,0)于是，定理的假設部分可以改寫成代數(shù)等式的形式。

由假設，條件（1）可以寫成：(A在圓O上)；

(B在圓O上)；(C在圓O上)；O定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。第一步幾何問題的代數(shù)化為了簡便，可以將△ABC的外接圓中心O取為De條件（2）可以寫成：(R在BC上)

(S在AC上)(T在AB上)O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。條件（2）可以寫成：(R在BC上)(S在AC上)(T在條件（3）可以寫成：要證明的結論可以表示為(R,S,T共線)O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。條件（3）可以寫成：要證明的結論可以表示為(R,S,T至此,我們已經完成了用吳方法證明幾何定理的第一步：用解析幾何方法將幾何問題代數(shù)化。當然，也可以用其他方法,如三角方法。所得代數(shù)形式的問題就是，在假設一組多元多項式組為0的條件下，求證另一多項式為0。即，定理的等價代數(shù)表示為求證(R,S,T共線)設(A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O至此,我們已經完成了用吳方法證明幾何定理的第一步：用解析幾何等價地,用多項式的零點集（集合論）描述上述定理：需要證明問題的進一步轉換。O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T

共線。如何做?用記號問題的進一步轉換。O定理：如何做?用記號由此,我們有零點關系有方程組的關系已經對約化。對任意兩個一元多項式我們總有若帶余除法的回憶由此,我們有零點關系有方程組的關系已經對約化。對對現(xiàn)在的問題，如果能實現(xiàn)就有定理就成立，遺憾的是(*)一般不成立!!什么條件下成立呢？對現(xiàn)在的問題，如果能實現(xiàn)就有定理就成立，遺憾的是(*)一般不第二步整序就本例而論，A,B,C三點在圓上的位置定了，其他點的位置也就定了。而A,B,C三點的位置可以由三個縱坐標來確定。因此，在這12個變元當中,只有3個是自由的，另外9個都是受約束的。我們取為自由變元，并用另外記號記

整序就是把約束變元排個序改變?yōu)榱硪蛔寰哂刑厥饨Y構的多項式組，并盡可能零點性質不變。然后通過讓滿足我們所要的結論。O第二步整序就本例而論，A,B,C三點在圓上的位置定了，其他無規(guī)律(A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O已知無規(guī)律(A在圓O上)(B在圓O上)(C在圓O上)(R在BC把左邊看作多元多項式，讓等價地變?yōu)槿切涡问狡渲腥绾蔚玫降?？有?guī)律O把左邊看作多元多項式，讓等價地變?yōu)槿切涡问狡渲腥绾蔚玫降?？的推導因為利用簡化后得?A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O用消，令的推導因為利用簡化后得令(A在圓O上)(類似地得到其它的使得類似地得到其它的使得故，要證明的問題變?yōu)樽C明的問題。因為=故，要證明的問題變?yōu)樽C明的問題。因為=吳方法的第二步至此完成。我們得到了一個三角化組(升列)：第三步:偽除法

(其它變元暫看成擴域當中的常量)即對G進行帶余除法(稱偽除法);所得得余式稱為G關于對變元的偽余式,并用*9F記作做這種偽除時，需要假定這叫做非退化條件。

這相當于從方程解出再將該解帶入中。和G開始。將G和都看成最后一個約束變元的一元多項式偽除求余從吳方法的第二步至此完成。我們得到了一個三角化組(升列)：第三現(xiàn)將看成的(一元)多項式，即寫成

又將也看成的多項式，并用偽除得到的偽余式,即再將和都看成的多項式。用偽除求余式,并繼續(xù)下去?，F(xiàn)將看成的(一元)多項式，即寫成又將也看成的多項式，并用從這個等式看出,當?shù)臈l件下,有最后得到等式其中所要證明定理的結論成立。成立。這表明在非退化條件之下，從這個等式看出,當?shù)臈l件下,有最后得到等式其中所要證明定理的偽除法求余式，若用手算則是繁瑣的，甚至是不可行的。它有時要涉及上千項的多項式的運算和整理。如果我們有足夠細心并有足夠的耐心，也許可以用紙筆來完成這個例子中的計算，但可能要花上好幾個小時。若要是算到最后余式不為零，根據(jù)吳方法：若升列不可約的，則命題不成立．對可約升列，總可以通過因子分解將其化為幾個不可約升列，從而將問題完全解決。整個過程的基本思想是樸素的：盡可能地消去約束變元，或降低約束變元的次數(shù)，使定理的假設部分三角化，再用其將定理的結論約化為0。注：偽除法求余式，若用手算則是繁瑣的，甚至是不可行的。它有時要涉第四步:退化條件的討論從形式上看，非退化條件就是要求在整序后得到的升序中，每個多項式中新出現(xiàn)的約束變元最高次項的系數(shù)不等于零．在本例中，多項式不產生非退化條件。多項式中新出現(xiàn)的約束變元是，它的最高次項是1次的，系數(shù)是，因而產生了非退化條件

該條件的幾何意義是“B與C兩點不重合”．這當然是需要的：如果B與C重合，那么ABC就不成為三角形了。提出要對“非退化條件”進行研究是吳文俊教授對幾何證明理論的又一貢獻，也是定理機器證明研究的副產品．長期以來，人們認為Euclid幾何中的論證推理過程是嚴密．即使有問題，也出在公理體系上。D.Hilbert重整了Euclid公理體系之后，總不會再有什么漏洞了吧?但吳文俊教授指出：傳統(tǒng)的初等幾何證明方法不但不嚴密，而且也不可能嚴密。問題就出在“退化”情形上。

O第四步:退化條件的討論從形式上看，非退化條件就是要求在整序那么，在幾何命題的假設中，排除了退化情形，是不是就萬事大吉，完全嚴密了呢?問題沒這么簡單；因為用綜合法證幾何題，往往要作輔助線、輔助圖，再對輔助圖形運用一些已知定理。在輔助圖形中有可能遇到退化的情形。怎樣作輔助線，事先是不知道的，因而無法預先說明會出現(xiàn)哪些退化情形而使證明失效。證明中推理環(huán)節(jié)越多，出現(xiàn)退化情形而破壞證明的嚴密性的可能性就越大。吳方法使這個問題得到了圓滿解決：在機器證明幾何定理的過程中，該方法能夠自然地一一給出退化情形的代數(shù)表示，指出保證命題成立的非退化條件。Euclid幾何中的概念通常是排除了”退化’’情形．比如說“三角形’’，就要求三頂點不共線，若三頂點共線，三角形成了線段，就是退化了。有些幾何定理，對退化情形也成立；但也有些幾何定理，圖形一退化，定理便不成立了。例如“△ABC中，若∠B=∠C，則“|AB|=IACI”，這條定理，當∠B=∠C=0時就不成立，而當∠B=∠C=時又成立了。由此可見，對退化條件要單獨進行討論。

O那么，在幾何命題的假設中，排除了退化情形，是不是就萬事大吉，七，總結七，總結為什么能機械化？算法是構造性的，可以程序化理論是嚴密的。數(shù)學原理是核心，計算機是輔助工具。為什么能機械化？算法是構造性的，可以程序化數(shù)學原理是核心，八、對吳方法的評價八、對吳方法的評價吳方法遵循中國傳統(tǒng)數(shù)學中幾何代數(shù)化的思想，與通?；跀?shù)理邏輯的方法根本不同，首次實現(xiàn)了高效的幾何定理自動證明，顯現(xiàn)了無比的優(yōu)越性。他的工作被稱為自動推理領域的先驅性工作，并于1997年獲得“Herbrand自動推理杰出成就獎”。在授獎辭中對他的工作給了這樣的介紹與評價:

“幾何定理自動證明首先由赫伯特·格蘭特(H.Gerlenter)于50年代開始研究。雖然得到一些有意義的結果，但在吳方法出現(xiàn)之前的20年里，這一領域進展甚微。在不多的自動推理領域中，這種被動局面是由一個人完全扭轉的。吳文俊很明顯是這樣一個人。他將幾何定理證明從一個不太成功的領域變?yōu)樽畛晒Φ念I域之一。”吳方法遵循中國傳統(tǒng)數(shù)學中幾何代數(shù)化的思想，與通?；跀?shù)理邏輯

公理化體系的幾何定理證明非常不機械化。以中學課程中的幾何為例，－個定理的證明，往往要經過冥思苦想，奇巧構思，無章可循地填加輔助線，迂回曲折地給出證明。如何利用計算機進行自動推理，特別是進行幾何定理的自動證明，是學術界長期研究的課題。

公理化體系的幾何定理證明非常不機械化。以中學課程中

吳先生創(chuàng)立的初等幾何（泛指不具有微分運算的幾何，如歐氏幾何、非歐幾何、仿射幾何、投影幾何、代數(shù)幾何等等）定理證明的機械化方法（國際上稱“吳方法”）打破了國際自動推理界在幾何定理自動證明研究中長期徘徊不前的局面，也使我國在這一領域處于領先地位。吳先生創(chuàng)立的初等幾何（泛指不具有微分運算的幾何，

機器證明定理的研究的推動下，一門研究如何用計算機進行符號與代數(shù)計算的學科--計算機代數(shù)--應運而生了。計算機代數(shù)系統(tǒng)如Mathematica和Maple為定理機器證明的研究和發(fā)展提供了物質基礎。吳方法的發(fā)現(xiàn)使具有數(shù)千年歷史，手工式的初等幾何研究真正跨入了機械化的階段。今后，當人們在初等幾何范圍內提出新命題而不知其真假時，只要上機一試，便知分曉，把煩瑣復雜計算交給計算機，而人把精力投入到更深刻創(chuàng)造發(fā)明當中。機器證明定理的研究的推動下，一門研究如何用計算機九、吳方法的廣泛應用九、吳方法的廣泛應用控制論、曲面拼接問題、機構設計、化學平衡問題、平面天體運行的中心構形等，還建立了解決全局優(yōu)化問題的新方法。吳方法還被用于若干高科技領域，得到一系列國際領先的成果，包括曲面造型、機器人結構的位置分析、智能計算機輔助設計(CAD)、信息傳輸中的圖像壓縮等。控制論、曲面拼接問題、機構設計、化學平衡問題、平面天體從開普勒定律到牛頓定律

開普勒定律為（1）行星繞太陽以橢圓軌道運行，太陽為一焦點（2）太陽到行星的向量在相同的時間掃過相同的面積牛頓定律為（3）行星的加速度與太陽到行星的距離的平方成反比利用吳方法在微分域上的推廣，可以從開普勒經驗公式自動推導出牛頓定律。從開普勒定律到牛頓定律開普勒定律為微分幾何定理機器證明

微分幾何離不開函數(shù)和微分，從表面上看似乎不能使用計算機進行證明，但事實上并非如此。在微分幾何中出現(xiàn)的那種函數(shù)與導數(shù)完全可以形式地來對待，因此，存在著通過有限次的構造步驟借助于計算機來進行微分幾何定理證明的可能性。微分多項式組的整序算法已經應用于微分幾何的一些定理的機器證明與一些幾何關系或公式的自動發(fā)現(xiàn)和推導。微分幾何定理機器證明微分幾何離不開函數(shù)和微分，從表面上機器人與連桿機構的運動分析

如圖，綠色的平臺是活動平臺，下面的平臺是固定的，六根連桿長度可變，求連桿長度變化時平臺上一點的軌跡。機器人與連桿機構的運動分析如圖，綠色的平臺是活動平臺機器人與連桿機構的運動分析

已知連桿機構的構成，求該機構上某一點的軌跡及該點的位置與連桿機構的關系，這類問題稱為機械設計中的正解問題。前面的例子就是一個正解問題。反過來，求解連桿機構的參數(shù)使得連桿機構上一點恰好位于空間指定位置的問題稱為機械設計中的逆解問題。這兩類問題都可以看成方程求解問題。吳文俊用特征集方法解決了一般PUMA型機器人的逆解問題，研究了四連桿的設計問題。機器人與連桿機構的運動分析已知連桿機構的構成，求該機構曲面連接問題

在幾何設計中，有一大類問題要確定一給定次數(shù)的代數(shù)曲面按一定要求連接已給的若干代數(shù)曲面。這類問題可以用吳方法解決。左圖是一個連接三根管道的例子。曲面連接問題在幾何設計中，有一大類問題要確定一給定次數(shù)的左楊-Baxter方程與量子群

應用吳方法，采用人機對話的方式，運用多種技巧，成功地求出二維楊-Baxter方程的全部解。在二維情形下，這組方程有16個未知數(shù)，由64個三次多項式方程組成。相應于楊-Baxter方程的解，可得到量子群。但具體計算對應的量子群并不容易。從吳方法出發(fā)，可給出依據(jù)楊-Baxter方程的解直接計算相應量子群的機械化方法。楊-Baxter方程與量子群應用吳方法，采用人機對話的數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件結束語結束語是思想是方法是技術數(shù)學是思想數(shù)學謝謝謝謝如何實現(xiàn)自動推理--簡明介紹數(shù)學機械化與吳方法講座2008-11-？朝魯上海海事大學數(shù)學系如何實現(xiàn)自動推理講座2008-11-？朝魯上海講座一、吳文俊簡介講座一、吳文俊簡介

吳文俊院士是中國科學院數(shù)學與系統(tǒng)科學研究院的研究員，我國著名的數(shù)學家。他于上世紀50年代對數(shù)學的主要領域—拓撲學做出了杰出貢獻。70年代后期，吳文俊開創(chuàng)了嶄新的數(shù)學機械化領域。他建立了用計算機證明幾何定理的“吳方法”。實現(xiàn)了高效幾何定理自動證明；吳方法應用于計算機圖形學、機器人、機構設計、全局優(yōu)化、化學平衡、天體運行……等領域。87歲≠不能創(chuàng)新

吳文俊院士獲得過很多獎項：1956年獲得國家自然科學一等獎1979年獲得中國科學院自然科學一等獎1990年獲得第三世界科學院數(shù)學獎1993年獲得陳嘉庚數(shù)理科學獎1994年獲得首屆香港求是科技基金會杰出科學家獎1998年度國際自動推理界的最高獎“Herbrand獎”

2000年獲得首屆國家最高科技獎2006年獲邵逸夫數(shù)學科學獎87歲≠不能創(chuàng)新吳文俊院士獲得過很多獎項：/detail2.asp?project_id=122&type_id=22看一段視頻報道/detail2吳文俊的虛擬軸機床——數(shù)學機械化方法及其在并聯(lián)機構中的應用

吳文俊院士開創(chuàng)了數(shù)學機械化研究領域。他所建立的“吳方法”，“吳消元法”及“吳有限核定理”已成為該領域的奠基性成果。運用數(shù)學機械化方法，本項研究解決了廣義Stewart平臺正解問題，這是對機器人運動學領域的一個主要貢獻。以此為基礎，研制成功我國第一臺大型虛擬軸機床樣機與集成電路制造裝備關鍵子系統(tǒng)。吳文俊的虛擬軸機床——數(shù)學機械化方法及其在并聯(lián)機構中的應用數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件二、腦力勞動能機械化嗎？二、腦力勞動能機械化嗎？勞動=體力勞動+腦力勞動;

17世紀以來，工業(yè)革命使人們逐漸實現(xiàn)了體力勞動的機械化，大大地促進了社會生產力的發(fā)展。?!勞動=體力勞動+腦力勞動;17世紀以來，工業(yè)革命使人們逐漸

腦力勞動的徹底機械化是不可能，但部分機械化是完全可能，并且隨著人類智慧的提高這個機械化程度越來越高。意義深遠!腦力勞動的機械化是人類的追求,夢想腦力勞動的徹底機械化是不可能，但部分機械化是完全可能，并且

作為科學基礎的數(shù)學研究是典型的腦力勞動，具有論證嚴謹、表述明確等優(yōu)點，理應率先實現(xiàn)機械化。成為其他學科機械化的基礎。如今，人類社會正步入信息革命時代,計算機的功能不斷增強，為人類實現(xiàn)腦力勞動的機械化創(chuàng)造了物質條件。對腦力勞動的機械化，作為其靈魂或核心技術,數(shù)學的參與是不可缺少。作為科學基礎的數(shù)學研究是典型的腦力勞動，具有論證三、數(shù)學機械化

與自動推理三、數(shù)學機械化

吳文?。核^機械化，無非是刻板化和規(guī)格化。數(shù)學問題的機械化，就要求在運算或證明過程中，每前進一步之后，都有一個確定的、必須選擇的下一步，這樣沿著一條有規(guī)律的、刻板的道路，一直達到結論。數(shù)學機械化吳文俊：所謂機械化，無非是刻板化和規(guī)格化。數(shù)學機械自動推理機械化算法的計算機實現(xiàn)。對某一個思維問題(腦力勞動)要設計機械化算法;算法是構造化的,能轉化為計算機指令;計算機能接受并能按設計邏輯處理這些指令,推理出結論.這里要知道兩個關鍵點:計算機能處理什么?算法是構造性(機械化)?自動推理機械化算法的計算機實現(xiàn)。實現(xiàn)機械化和自動推理需要兩個發(fā)展：

構造性數(shù)學的發(fā)展（腦子）；計算機的發(fā)展（肢體）。出現(xiàn)了“數(shù)學機械化”、“自動推理”、“計算機代數(shù)”,“理論計算機”，……等學科。實現(xiàn)機械化和自動推理需要兩個發(fā)展：出現(xiàn)了“數(shù)學機四、數(shù)學機械化的艱難歷程

——從設想到實現(xiàn)四、數(shù)學機械化的艱難歷程數(shù)學機械化：從設想到實現(xiàn)笛卡爾萊布尼茨希爾伯特數(shù)學機械化：從設想到實現(xiàn)笛卡爾萊布尼茨希爾伯特數(shù)學機械化：從設想到實現(xiàn)哥德爾塔斯基王浩吳文俊數(shù)學機械化：從設想到實現(xiàn)哥德爾塔斯基王浩吳文俊笛卡爾的設想

17

世紀法國的數(shù)學家Descartes曾有過一個偉大的設想：“一切問題化為數(shù)學問題，一切數(shù)學問題化為代數(shù)問題，一切代數(shù)問題化為代數(shù)方程求解問題?！?/p>

并，Descartes

沒有停留在空想，他所創(chuàng)立的解析幾何，在空間形式和數(shù)量關系之間架起了一座橋梁，實現(xiàn)了初等幾何問題的代數(shù)化。但，Descartes把問題想得太簡單了，如果他的設想真能實現(xiàn)，那就不僅是數(shù)學的機械化，而是全部科學的機械化。笛卡爾的設想萊布尼茲之夢德國數(shù)學家Leibniz

曾有過“推理機器”的設想。他研究過邏輯，設計并制造出能做乘法的計算機，進而萌發(fā)了設計萬能語言和造一臺通用機器的構想。他認為,他的方案一旦實現(xiàn),人們之間的一切爭論都可以被心平氣和的機器體力勞動所代替。他的努力促進了Boole代數(shù)、數(shù)理邏輯以及計算機科學的研究，正是沿著這一方向，經后人的努力，形成了機器定理證明的邏輯方法。

萊布尼茲之夢德國數(shù)學家Leibniz曾有過“推理機器”的希爾伯特的構想

Hilbert在《幾何基礎》中提出了從公理化走向機械化的數(shù)學構想。Hilbert計劃將數(shù)學知識納入嚴格的公理體系中，并著力在公理化基礎上尋找機械化的方法判定命題是否成立。Hilbert同時指出，定理的判定問題應當是分類解決的，解決方法要同時強調簡單性和嚴格性。在Hilbert

的名著《幾何基礎》一書中就提供了一條可以對一類幾何命題進行機械化判定的定理—當然，在那個時代，不僅Hilbert

本人，整個數(shù)學界都沒有意識到這一點。

希爾伯特的構想Hilbert在《幾何基礎》哥德爾的著名結果

G?del著名的不完全性定理指出一個不弱于初等數(shù)論的形式系統(tǒng)如果是無矛盾的，則是不完全的，即存在形式系統(tǒng)的一個命題，它和它的否定都不能由形式系統(tǒng)證明。因此，Hilbert的要求太高了。上述的G?del不完全性定理斷言：即使在初等數(shù)論的范圍內，對所有命題進行判定的機械化方法也是不存在的！哥德爾的著名結果G?del著名的不完全性定理塔斯基的判定法

波蘭數(shù)學家Tarski

在1950年推廣了關于代數(shù)方程實根數(shù)目的Sturm法則，由此證明了一個引人注目的定理：“一切初等幾何和初等代數(shù)范圍的命題，都可以用機械方法判定?！?/p>

Tarski得出的結論給定理證明機械化的研究帶來了曙光?？上姆椒ㄌ珡碗s，即使用高速計算機也證明不了稍難的幾何定理。

塔斯基的判定法波蘭數(shù)學家Tarski在1950王浩：邁向數(shù)學機械化1959年，王浩設計了一個程序，用計算機證明了Russell、Whitehead的巨著《數(shù)學原理》中的幾百條有關命題邏輯的定理，僅用了9分鐘。王浩工作的意義在于宣告了用計算機進行定理證明的可能性。在1960年的《IBM研究與發(fā)展年報》（IBMJournal）上，王浩發(fā)表了《邁向數(shù)學機械化》（TowardMechanicalMathematics）的文章?！皵?shù)學機械化”一詞即出自此處。王浩：邁向數(shù)學機械化1959年，王浩設計了一個程序，

其他人與王浩同一時期，A.Newell和H.A.Simon也做了與王浩類似的工作。1965年Robinson歸結原理的提出是用邏輯方法進行機器證明的又一重要進展。1976年K.I.Appel和W.Haken在高速電子計算機上用1200小時的計算時間，證明了著名的四色定理，使數(shù)學家們100多年來未能解決的這個難題得到了肯定的回答（機械化證明）。數(shù)學機械化自動推理計算機代數(shù)-上海海事大學課件數(shù)學大師們的堅持不懈地追求,表明數(shù)學機械化思想重要而深刻。但數(shù)學機械化歷程漫長而艱難，發(fā)展緩慢。70年代末，在中國得到突破！數(shù)學大師們的堅持不懈地追求,表明數(shù)學機械化思想重要而深刻。

五、數(shù)學機械化的突破

——吳方法的出現(xiàn)五、數(shù)學機械化的突破吳文?。?/p>

數(shù)學機械化（機器證明）領域的新的一頁

1976年，我國數(shù)學家吳文俊教授為數(shù)學機械化（機器證明，自動推理）的發(fā)展翻開了新的一頁。提出幾何定理的機器證明機械化算法，并計算機實現(xiàn)。他當時既沒有接觸到Tarski的工作,也沒有想到Hilbert的著作里那一條定理。中國古代構造性數(shù)學思想的啟迪了他。吳文?。?/p>

數(shù)學機械化（機器證明）領域的新的一頁1971977年，吳文俊在《中國科學》上發(fā)表論文《初等幾何判定問題與機械化問題》。1984年，吳文俊的學術專著《幾何定理機器證明的基本原理》由科學出版社出版，這部專著著重闡明幾何定理機械化證明的基本原理。1985年，吳文俊的論文《關于代數(shù)方程組的零點》發(fā)表，具體討論了多項式方程組所確定的零點集。與國際上流行的代數(shù)理想論不同，明確提出了具有中國自己特色的、以多項式零點集為基本點的機械化方法。自此，“吳方法”宣告誕生，數(shù)學機械化研究揭開了新的一幕。

1977年，吳文俊在《中國科學》上發(fā)表論文《初等幾何判定問

六、吳方法的介紹六、吳方法的介紹

所謂定理的機械化證明，就是對一類定理（這類定理可能成千上萬）提供一種統(tǒng)一的方法，使得該類定理中每個定理，都可依此方法給出證明。在證明過程中，每前進一步，都有章可循地確定下一步該做什么和如何做。

從“一理一證”到“－類一證”，是數(shù)學的認識和實踐的飛躍。數(shù)學(腦力勞動)機械化的典范所謂定理的機械化證明，就是對一類定理（這類吳方法的基本思想是十分樸素的:把幾何命題化成代數(shù)形式加以處理?；墒裁葱问?如何處理?整個過程是什么樣?主要思想是什么?吳方法的基本思想是十分樸素的:

Simson定理的機器證明

Simson定理：在的外接圓上任取一點P。自P點向直線BC,CA,AB引垂線,垂足依次為R,S,T，那么R,S,T三點在一直線上(如圖所示)。O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:R,S,T共線。用一個例子來簡單介紹吳方法Simson定理的機器證明Simson定理：在

為了簡便，可以將△ABC的外接圓中心O取為Descartes坐標原點，將圓半徑取為單位長，并設各點的坐標為

A(x1,y1)，B(x2,y2)，C(x3,y3)，R(x4,y4)，S(x5,y5)，T(x6,y6)，P(1,0)于是，定理的假設部分可以改寫成代數(shù)等式的形式。

由假設，條件（1）可以寫成：(A在圓O上)；

(B在圓O上)；(C在圓O上)；O定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。第一步幾何問題的代數(shù)化為了簡便，可以將△ABC的外接圓中心O取為De條件（2）可以寫成：(R在BC上)

(S在AC上)(T在AB上)O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。條件（2）可以寫成：(R在BC上)(S在AC上)(T在條件（3）可以寫成：要證明的結論可以表示為(R,S,T共線)O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T共線。條件（3）可以寫成：要證明的結論可以表示為(R,S,T至此,我們已經完成了用吳方法證明幾何定理的第一步：用解析幾何方法將幾何問題代數(shù)化。當然，也可以用其他方法,如三角方法。所得代數(shù)形式的問題就是，在假設一組多元多項式組為0的條件下，求證另一多項式為0。即，定理的等價代數(shù)表示為求證(R,S,T共線)設(A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O至此,我們已經完成了用吳方法證明幾何定理的第一步：用解析幾何等價地,用多項式的零點集（集合論）描述上述定理：需要證明問題的進一步轉換。O

定理：

(1)A,B,C,P在同一圓上;

條件：(2)R,S,T分別在直線BC,CA,AB上;

(3)PR⊥BC,PT⊥AB,PS⊥AC

結論:

R,S,T

共線。如何做?用記號問題的進一步轉換。O定理：如何做?用記號由此,我們有零點關系有方程組的關系已經對約化。對任意兩個一元多項式我們總有若帶余除法的回憶由此,我們有零點關系有方程組的關系已經對約化。對對現(xiàn)在的問題，如果能實現(xiàn)就有定理就成立，遺憾的是(*)一般不成立!!什么條件下成立呢？對現(xiàn)在的問題，如果能實現(xiàn)就有定理就成立，遺憾的是(*)一般不第二步整序就本例而論，A,B,C三點在圓上的位置定了，其他點的位置也就定了。而A,B,C三點的位置可以由三個縱坐標來確定。因此，在這12個變元當中,只有3個是自由的，另外9個都是受約束的。我們取為自由變元，并用另外記號記

整序就是把約束變元排個序改變?yōu)榱硪蛔寰哂刑厥饨Y構的多項式組，并盡可能零點性質不變。然后通過讓滿足我們所要的結論。O第二步整序就本例而論，A,B,C三點在圓上的位置定了，其他無規(guī)律(A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O已知無規(guī)律(A在圓O上)(B在圓O上)(C在圓O上)(R在BC把左邊看作多元多項式，讓等價地變?yōu)槿切涡问狡渲腥绾蔚玫降模坑幸?guī)律O把左邊看作多元多項式，讓等價地變?yōu)槿切涡问狡渲腥绾蔚玫降模康耐茖б驗槔煤喕蟮昧?A在圓O上)

(B在圓O上)(C在圓O上)(R在BC上)(S在AC上)(T在AB上)O用消，令的推導因為利用簡化后得令(A在圓O上)(類似地得到其它的使得類似地得到其它的使得故，要證明的問題變?yōu)樽C明的問題。因為=故，要證明的問題變?yōu)樽C明的問題。因為=吳方法的第二步至此完成。我們得到了一個三角化組(升列)：第三步:偽除法

(其它變元暫看成擴域當中的常量)即對G進行帶余除法(稱偽除法);所得得余式稱為G關于對變元的偽余式,并用*9F記作做這種偽除時，需要假定這叫做非退化條件。

這相當于從方程解出再將該解帶入中。和G開始。將G和都看成最后一個約束變元的一元多項式偽除求余從吳方法的第二步至此完成。我們得到了一個三角化組(升列)：第三現(xiàn)將看成的(一元)多項式，即寫成

又將也看成的多項式，并用偽除得到的偽余式,即再將和都看成的多項式。用偽除求余式,并繼續(xù)下去?，F(xiàn)將看成的(一元)多項式，即寫成又將也看成的多項式，并用從這個等式看出,當?shù)臈l件下,有最后得到等式其中所要證明定理的結論成立。成立。這表明在非退化條件之下，從這個等式看出,當?shù)臈l件下,有最后得到等式其中所要證明定理的偽除法求余式，若用手算則是繁瑣的，甚至是不可行的。它有時要涉及上千項的多項式的運算和整理。如果我們有足夠細心并有足夠的耐心，也許可以用紙筆來完成這個例子中的計算，但可能要花上好幾個小時。若要是算到最后余式不為零，根據(jù)吳方法：若升列不可約的，則命題不成立．對可約升列，總可以通過因子分解將其化為幾個不可約升列，從而將問題完全解決。整個過程的基本思想是樸素的：盡可能地消去約束變元，或降低約束變元的次數(shù)，使定理的假設部分三角化，再用其將定理的結論約化為0。注：偽除法求余式，若用手算則是繁瑣的，甚至是不可行的。它有時要涉第四步:退化條件的討論從形式上看，非退化條件就是要求在整序后得到的升序中，每個多項式中新出現(xiàn)的約束變元最高次項的系數(shù)不等于零．在本例中，多項式不產生非退化條件。多項式中新出現(xiàn)的約束變元是，它的最高次項是1次的，系數(shù)是，因而產生了非退化條件

該條件的幾何意義是“B與C兩點不重合”．這當然是需要的：如果B與C重合，那么ABC就不成為三角形了。提出要對“非退化條件”進行研究是吳文俊教授對幾何證明理論的又一貢獻，也是定理機器證明研究的副產品．長期以來，人們認為Euclid幾何中的論證推理過程是嚴密．即使有問題，也出在公理體系上。D.Hilbert重整了Euclid公理體系之后，總不會再有什么漏洞了吧?但吳文俊教授指出：傳統(tǒng)的初等幾何證明方法不但不嚴密，而且也不可能嚴密。問題就出在“退化”情形上。

O第四步:退化條件的討論從形式上看，非退化條件就是要求在整序那么，在幾何命題的假設中，排除了退化情形，是不是就萬事大吉，完全嚴密了呢?問題沒這么簡單；因為用綜合法證幾何題，往往要作輔助線、輔助圖，再對輔助圖形運用一些已知定理。在輔助圖形中有可能遇到退化的情形。怎樣作輔助線，事先是不知道的，因而無法預先說明會出現(xiàn)哪些退化情形而使證明失效。證明中推理環(huán)節(jié)越多，出現(xiàn)退化情形而破壞證明的嚴密性的可能性就越大。吳方法使這個問題得到了圓滿解決：在機器證明幾何定理的過程中，該方法能夠自然地一一給出退化情形的代數(shù)表示，指出保證命題成立的非退化條件。Euclid幾何中的概念通常是排除了”退化’’情形．比如說“三角形’’，就要求三頂點不共線，若三頂點共線，三角形成了線段，就是退化了。有些幾何定理，對退化情形也成立；但也有些幾何定理，圖形一退化，定理便不成立了。例如“△ABC中，若∠B=∠C，則“|AB|=IACI”，這條定理，當∠B=∠C=0時就不成立，而當∠B=∠C=時又成立了。由此可見，對退化條件要單獨進行討論。

O那么，在幾何命題的假設中，排除了退化情形，是不是就萬事大吉，七，總結七，總結為什么能機械化？算法