幾何定理機器證明

類型

①第一類型

定理的特徵是假設部分的所有代數關係式對於某些特定變數都必須是線性的，包括一類構造型的純交點定理，其對應的機器證明方法稱為希爾伯特方法；

②第二類型定理

特徵是假設和終結部分的代數關係式都可用多項式的方程來表示，其對應的機器證明方法是中國數學家吳文俊首先提出的,稱為吳文俊方法;

③第三類型定理

特徵是假設和終結部分可以是任意的多項式等式或不等式，但其係數必須在一實閉域中，因而原來的幾何必須有次序關係，其對應的機器證明方法稱為塔斯基方法。這三種方法各有其適用範圍，但就可以通用的那些定理證明問題來說，希爾伯特法效率最高而塔斯基法效率最低，但是前者的適用範圍很窄。1980年在 HP9835A機上，用吳文俊方法成功地證明了勾股定理、西姆遜線定理、帕普斯定理、帕斯卡定理、費爾巴哈定理,並在45個帕斯卡點中發現了20條帕斯卡圓錐曲線,這種方法還推廣到微分幾何，將微分幾何曲線論中的貝屈朗定理推廣到仿射微分幾何。吳文俊的研究成果引起了國際學術界的重視。

幾何定理機器證明的幾種主要方法

代數方法

幾何定理機器證明的代數方法又包含多種不同的方法，如吳方法、Grobner 基方法、單點例證法、數值並行法等。其中，吳方法是代數方法的代表，其它幾種方法都是在吳方法之後，受其思想的影響提出來的。吳方法是我國著名數學家吳文俊先生1977年提出來的一種用代數的方法來證明幾何定理的新的方法。該方法適用於證明“等式型”的幾何定理，而且證明的效率很高，一般可以用幾分鐘甚至幾秒鐘就可以證出不簡單的定理。其中，等式型幾何定理是指：將幾何問題引進坐標化為代數問題後，問題的條件和結論都可以化為若干個等式的形式。

吳方法進行幾何定理機器證明的第一步是幾何問題代數化，建立坐標系，並將命題涉及的幾何圖形的點選取適當的坐標，然後把命題的條件和結論表示為坐標的多項式方程組。最後判斷條件方程組的解是否滿足結論方程。通常的幾何命題涉及的多項式方程組都是非線形的，一般無法將約束變元求出。吳方法是利用偽除法判定條件方程組的解是否是結論方程組的解。而且利用吳方法不僅可以判斷定理的正確與否，還可以自動找出定理賴以成立的非退化條件，這是傳統的做法無法做到的。多項式的偽余除法可以通過計算機做符號計算進行。此外，單點例證法和數值並行法，這兩種方法與吳方法進行大量符號計算不同，主要利用數值計算的方法進行定理的證明，所以有時也被單獨列為一類方法，即幾何定理證明的數值方法。數值方法與其它方法相比，具有效率高的優點。

幾何不變數

以吳方法為代表的代數方法僅僅能夠判斷幾何命題的成立與否，證明的過程十分複雜，而且需要進行大量的數值計算和符號計算，這與傳統幾何證明的簡潔明了大相逕庭。人們難以讀懂這種方法生成的證明，往往只能得出命題真假的結論，因此很多人難以接受這種證明的風格。如何生成讓人容易讀懂的幾何證明過程這一問題成為科學家面臨的又一個嚴峻的挑戰。 1992年，中科院院士張景中教授以其多年研究的面積法為基礎，提出了幾何定理機器證明的新方法，基於幾何不變數的消點法。隨後，它與周鹹青、高小山合作完善了該方法，並編寫了程式，終於成功的利用計算機對大量非平凡的幾何命題生成了簡潔易讀的幾何證明，這一傑出的工作被譽為計算機處理幾何問題的里程碑。消點法包括一組構圖規則、一組幾何不變數以及一組消點公式。該方法的基本思想是：利用構圖規則將欲證幾何命題中涉及的圖形構造出來，並在構圖的過程中生成關於點的約束條件，同時將欲求證的命題表示成圖中幾何量的等式的形式，然後利用消點公式，按照點在作圖時出現的相反順序，依次從結論等式中消去，最終結論等式會化為顯然成立的等式。後來，楊路教授又將消點法拓展到非歐幾何，成功的證明和發現了大量的新的非歐幾何定理。李洪波博士、楊海圈博士也在面積不變數的基礎上提出用向量法實現幾何定理的可讀證明，即Clifford代數法，也取得了很好的效果。