吳文俊方法

吳文俊方法(Wu Wenjun method)一種定理機器證明方法.是由吳文俊創立並加以系統化和完善的定理機器證明方法，簡稱吳方法.吳方法以構造性的代數幾何理論為工具，將幾何定理的求證問題，經坐標化和代數化之後，轉變成判定兩個代數簇的有條件的包含關係

，再加以解決.套用吳方法建立的程式系統已經證明了數百條高難度的幾何定理，同時還發明了若干新定理.吳方法還可用於證明非歐氏幾何中的定理，並能證明若干微分幾何定理，及解決微分方程中的某些定性問題. 用吳方法判定一個命題，其本質是判定一組多項式的公共零點集是否被包含於另一多項式的零點集的問題.分三步進行:第一步是把所給命題化為代數形式.第二步是整序，即把刻畫命題條件的多項式組PS經整序化為升列AS.第三步是求余，即將刻畫命題結論的多項式g對升列AS約化求餘式R. 若R為。，即可斷定命題在非退化條件I1IZ ...1k並。之下成立，或者說命題一般成立.其中111:…I*是升列AS中各多項式的初式之積.若R不為0，則當AS為不可約升列時，可斷定命題不真.