非退化條件(nondegenerate condition)是使幾何命題不失一般性的條件。吳文俊最先明確指出：幾何中一個有意義的定理，往往要附加若干限制條件，如平行四邊形ABCD的對角線AC與BD互相平分，其限制條件是ABCD必須是非退化的平行四邊形，即A，B，C，D四點不能在同一直線上。這樣的限制條件就稱為幾何定理的非退化條件。
基本介紹
- 中文名：非退化條件
- 外文名：nondegenerate condition
- 領域：數學
- 性質：定理機器證明方法
- 定義：使幾何命題不失一般性的條件
- 最先提出者：吳文俊
概念,弱非退化條件,人物簡介,格若勃基方法,機器證明,
概念
非退化條件(nondegenerate condition)是使幾何命題不失一般性的條件。吳文俊最先明確指出：幾何中一個有意義的定理，往往要附加若干限制條件，如平行四邊形ABCD的對角線AC與BD互相平分，其限制條件是ABCD必須是非退化的平行四邊形，即A，B，C，D四點不能在同一直線上。這樣的限制條件就稱為幾何定理的非退化條件。
吳方法的精美處之一就是，整序過程中可以確定出一類非退化條件。具體地，從假設條件的多項式組經整序得到升列f1，f2，…，fs後，記fj的初式為Ij，則吳氏非退化條件為I1I2…Is≠0。當結論多項式g關於升列f1，f2，…，fs的餘式為0時，升列f1，f2，…，fs的任一零點，只要滿足非退化條件，就一定是g的零點。若不滿足非退化條件，則可能不是g的零點。吳氏非退化條件另一套用是：若升列是由一多項式組PS整序而得到，則升列的零點滿足非退化條件時，必為PS的零點。
使用格若勃基方法證明定理時，也會產生非退化條件——要求基的表達式中分母不為0。從同一多項式出發，所得到的吳氏非退化條件與格若勃基非退化條件不一定相同。
弱非退化條件
吳氏非退化條件的改進。由張景中、楊路等人提出.吳氏非退化條件要求升列中多項式初式不為0，即多項式關於主變元的最高次項係數不為0。弱非退化條件則只要求主變元各項係數不同時為0。例如，設
f1=x-u，f2=(x+2u)y-(3x+2u)y+(u+1)， g=u(2x+1)y-(3+2x)uy+x(u+1)。
欲判斷在條件f1=f2=0之下是否有g=0，可按吳方法求g關於升列{f1，f2}的餘式，結果餘式為0。於是得到結論：在非退化條件x+2u≠0滿足時，由f1=f2=0可得g=0。但由弱非退化條件，此結論可改進為：若(x+2u)，(3x+2u)，(u+1)不同時為0，則由f1=f2=0可得g=0。但又因(x+2u)，(3x+2u)，(u+1)顯然不能同時為0，故得出結論“由f1=f2=0可得g=0”。
人物簡介
吳文俊是數學家。上海人。1940年畢業於上海交通大學。1947年赴法國留學，先後在斯特拉斯堡、巴黎、法國科學研究中心進行數學研究，1951年獲博士學位。1951年回國後，歷任北京大學數學系教授，中國科學院數 學研究所研究員、副所長，中國科 學院系統科學研究所研究員、副所長、名譽所長、數學機械化研究中心 主任，中國數學會理事長，中國科學 院數學物理學部副主任，全國政協常務委員等職。1955年當選為中國 科學院物理學數學化學部委員。主 要從事拓撲學、機器證明學等方面的科學研究並取得多項突出成果， 是數學機械化研究的創始人之一， 為我國數學研究和科學事業的發展作出了重要貢獻。1951年的博士論 文《球纖維空間示性類理論》是對纖 維空間基本問題的重要貢獻。50年 代在示性類、示嵌類等研究方面取得了一系列突出成果，並有許多重 要套用，被國際數學界稱為“吳文俊 公式”、“吳文俊示性類”，已被編入許多名著。這項成果獲1956年國家 自然科學獎一等獎。60年代繼續進 行示嵌類方面的研究，獨創性地發 現了新的拓撲不變數，其中關於多 面體的嵌入和浸入方面的成果至今 仍居世界領先地位。在龐特雅金示 性類方面的成果，是拓撲學纖維叢 理論和微分流形的幾何學的一項基 本理論研究，有深刻的理論意義。 近年來創立了定理機器證明的吳文俊原理(國際上稱為吳氏方法)，實 現了初等幾何與微分幾何定理的機 器證明，達到了世界先進水平。這一重要創新改變了自動推理研究的面貌，在定理機器證明領域產生了 巨大影響，且有重要的套用價值， 它將引起數學研究方式的變革。這 方面的成果曾獲全國科學大會重大 成果獎和中國科學院科技進步獎一 等獎。在機器發現和創造定理的研 究方面也已取得重要成果。發表研 究論文數十篇，並有專著多種。
格若勃基方法
格若勃基方法是一種定理機器證明方法。是將格若勃基用於幾何定理機器證明的方法.格若勃基方法已用於幾百條幾何定理的證明，並能從給定前提條件導出多種有幾何意義的結論，以發現新定理.但在多數情形下，其效率不及吳方法.設要判定的命題已化為代數形式，假設條件可表示為：
hi(u1，u2，…，ud，x1，x2，…，xr)=0 (i=1，2，…，n)，
結論可表示為：g(u1，u2，…，ud，x1，x2，…，xr)=0。
格若勃基方法如下：
第一步：把x1，x2，…，xr看成變元，計算{h1，h2，…，hn}的格若勃基G，將g對G約化求出模G的正規形式。若其正規形式為0，則命題一般真(即在一組非退化條件下成立)。若不為0，則進行第二步。
第二步：引入新變數z，計算{h1，h2，…，hn，zg-1}的格若勃基。若此格若勃基為{1}，即僅含常數項——關於ui的多項式，則命題一般真。否則，命題不真。
在求取格若勃基的過程中，u1，u2，…，ud被看成參數，因而在格若勃基的表達式中，可能出現以u1，u2，…，ud為變元的分式。套用格若勃基證明定理時，要求這些分式的分母不為0。這也稱為非退化條件。
機器證明
計算機科學的重要研究方向之一，也是人工智慧領域的重要組成部分。原意是用機械的步驟判定數學命題的真假，現在一般指用計算機證明定理或推導公式。根據不同要求，可以提出一理一證、一類一證或一般通用的機器證明方法。其形式又可以採用計算機輔助證明或計算機自動證明。
機器證明是數學機械化研究的一項重要內容。在計算機出現以前，這一領域已經走過了漫長的道路.17世紀，萊布尼茨(Leibniz，G.W.)和笛卡兒(Descartes，R.)分別從建立通用證明器和引進坐標、化一切問題為代數問題這兩個角度，考慮了邏輯的和代數的機器證明問題。儘管當時的努力不足以取得明顯的進展，卻提出了有重大意義的研究方向。事實上，今天的機器證明理論，主要是沿著這兩個方向發展和完善起來的。其中，希爾伯特(Hilbert，D.)、塔爾斯基(Tarski，A.)、賀布蘭德(Herbrand，J.)和魯賓孫(Robinson，J.A.)分別做出了重要的貢獻.中國數學家吳文俊，從20世紀70年代後期開始致力於數學機械化及定理機器證明的研究，提出了一整套有效的、被國內外公認的吳方法或吳理論。吳理論本質上是採用代數方法研究機器證明.這一理論不但豐富了機器證明的內容，而且還帶動了其他研究方法的發展.在吳理論的影響下，近年來還出現了GB法、例證法、數值並行法和可讀性證明法等.這些方法的不斷發展與完善，無疑具有重要的意義.機器證明就其方法而言是一些能判定某些命題真假的機械化方法，即一些算法.算法的作用域是由若干具有確定形式的命題組成的集。也就是說，算法工作開始時輸入要檢驗的命題的前提與結論或只輸入前提.算法工作結束時的輸出可能有下列幾種：
1.簡單地斷言命題成立或不成立，即輸出命題的真值；
2.宣布算法對所輸入的命題無效；
3.輸出若干附加條件，並斷言在這些附加條件下命題的結論成立；
4.輸出證明的步驟；
5.輸出由前提能推出的多種結論。
實際上，上述描述不能包羅機器證明的各式各樣的描述與問題的提法，因為它是一個迅速發展而遠未成熟的研究領域。
