幾何定理機器證明

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

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

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

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

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

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

幾何不變量的方法雖然實現了一大類幾何定理的機器的可讀證明，但是這種方法得到的證明過程常常不符合人的思維習慣。而利用演繹數據庫的方法，根據幾何命題所給的條件、已知的公理、定理及公式等推理規則，通過大量的試驗匹配的方法進行證明似乎更符合人的思維習慣。這種方法也被譽為“大英博物館式的推理方法”，最早有這種設想的是H.Gelernter,J.R.Hanson和D.W.Loveland。它們於1960年聯合發表一篇文章中提出了從結論出發進行搜索的後推鏈方法。

到了1975年，A.J.Nevins又提出了前推鏈方法，但是仍不能實現為有效的算法和程序。隨後的幾十年裏，科學家基於這兩種推理設想進行了大量的探索，但始終收效不大。直到1996年，張景中、高小山、周鹹青提出了一個基於前推模式的“幾何信息搜索系統” （GISS），成功的證明了161個非平凡的幾何命題，收到了良好的效果。基於該方法進行了較多的研究，也成功設計了一些的定理證明系統，取得了不錯的效果。演繹數據庫方法的特點是：不僅給出了定理的證明，還可以生成一個幾何性質的數據庫。該數據庫包含了所給幾何圖形中能由系統內部所用幾何公理推導出來的所有幾何性質。例如：證明垂心定理，最終數據庫中包含下面的幾何信息——6個共線關係，6個共圓關係，24個等角關係，7個三角形相似關係，105個等比關係。可見得到的信息十分豐富，但是這也成為這種方法的一個瓶頸，即中間的幾何信息過度膨脹。因此針對這一問題進行了大量的改進。