幾何定理機器證明
正文
用計算機自動證明某一類型幾何定理，甚至某一種幾何全部定理的原理和方法。從理論角度看，幾何定理的機器證明要經歷公理化、代數化與坐標化、機械化等步驟，才能編製程序並在計算機上實現。可用機器證明的幾何定理（主要是初等幾何的定理）有三種不同類型，與之對應則有三種不同的機器證明方法。每一類型定理的機器證明都必須假設代數化與坐標化已經完成，而且可把幾何定理的證明問題化為一些代數關係式的處理問題。①第一類型定理的特徵是假設部分的所有代數關係式對於某些特定變數都必須是線性的，包括一類構造型的純交點定理，其對應的機器證明方法稱為希爾伯特方法；②第二類型定理的特徵是假設和終結部分的代數關係式都可用多項式的方程來表示，其對應的機器證明方法是中國數學家吳文俊首先提出的,稱為吳文俊方法;③第三類型定理的特徵是假設和終結部分可以是任意的多項式等式或不等式，但其係數必須在一實閉域中，因而原來的幾何必須有次序關係，其對應的機器證明方法稱為塔斯基方法。這三種方法各有其適用範圍，但就可以通用的那些定理證明問題來說，希爾伯特法效率最高而塔斯基法效率最低，但是前者的適用範圍很窄。1980年在 HP9835A機上，用吳文俊方法成功地證明了勾股定理、西姆遜線定理、帕普斯定理、帕斯卡定理、費爾巴哈定理,並在45個帕斯卡點中發現了20條帕斯卡圓錐曲線,這種方法還推廣到微分幾何，將微分幾何曲線論中的貝屈朗定理推廣到仿射微分幾何。吳文俊的研究成果引起了國際學術界的重視。參考書目
吳文俊著：《幾何定理機器證明的基本原理（初等幾何部分）》，科學出版社，北京，1984。
