關(guān)于作者
一個(gè)畢業(yè)于北京大學(xué)數(shù)學(xué)力學(xué)系，在中國科學(xué)院計(jì)算所、計(jì)算中心和網(wǎng)絡(luò)中心工作過，在澳大利亞科工組織DMS、香港浸會學(xué)院數(shù)學(xué)系和中國21世紀(jì)議程管理中心等處工作過，多次獲國家和中科院科技獎并享受政府特殊津貼的退休老頭。現(xiàn)在在【中國科普博覽】網(wǎng)“科學(xué)新語林”欄目里開設(shè)一個(gè)《數(shù)學(xué)與計(jì)算機(jī)》的個(gè)人專欄，愿和愛好數(shù)學(xué)與計(jì)算機(jī)的各界網(wǎng)友和青少年朋友，談?wù)剬?shù)學(xué)與計(jì)算機(jī)的看法、想法。
計(jì)算機(jī)證明（5）
張建中
2013年06月05日
8. 歐氏幾何及其重要意義
數(shù)學(xué)是一棵富有生命力的大樹，從它史前誕生之時(shí)起，就為自己的生存、發(fā)展而斗爭。這場斗爭經(jīng)歷了史前的幾個(gè)世紀(jì)和隨后有文字記載歷史的幾個(gè)世紀(jì)，最后終于在肥沃的希臘土壤中扎穩(wěn)了生存的根基，并且在一個(gè)較短的時(shí)期里茁壯成長起來了。在這個(gè)時(shí)期，它綻出了一朵美麗之花——?dú)W氏幾何。其他的花蕾也含苞欲放。
這些公理、公設(shè)就是《幾何原本》全書的基礎(chǔ)。全書以這些公理和定義為依據(jù)，邏輯地展開它的各個(gè)部分。比如后面出現(xiàn)的每一個(gè)定理都寫明什么是已知、什么是求證，都要根據(jù)前面的定義、公理、定理進(jìn)行邏輯推理給予仔細(xì)證明。
從歐幾里得發(fā)表《幾何原本》到現(xiàn)在已有兩千多年，盡管科學(xué)技術(shù)日新月異，但歐氏幾何仍舊是中學(xué)生學(xué)習(xí)數(shù)學(xué)基礎(chǔ)知識的好教材。長期以來，人們都認(rèn)為《幾何原本》是兩千多年來傳播幾何知識的標(biāo)準(zhǔn)教科書，在西方是除了《圣經(jīng)》以外銷路最廣的一本書。由于歐氏幾何具有鮮明的直觀性并和邏輯演繹方法密切相結(jié)合等特點(diǎn)，長期實(shí)踐表明，它是培養(yǎng)、提高青少年邏輯思維能力的好教材，很多家長以此訓(xùn)練孩子的推理能力。歷史上不知有多少科學(xué)家從歐氏幾何學(xué)習(xí)中得到培養(yǎng)和訓(xùn)練，從而提高了科學(xué)研究的興趣和能力及基礎(chǔ)素質(zhì)，為人類作出了偉大的貢獻(xiàn)。此外，歐氏幾何還具有高超的美學(xué)價(jià)值，隨著幾何學(xué)美妙結(jié)構(gòu)和精確推理的發(fā)展，數(shù)學(xué)變成了一門藝術(shù)。
9. 幾何定理計(jì)算機(jī)證明的方法
從數(shù)學(xué)眾多分支角度上看，幾何在數(shù)學(xué)中歷史地位突出，在數(shù)學(xué)教育中的作用重要，因此對幾何定理進(jìn)行計(jì)算機(jī)證明成了數(shù)學(xué)定理證明領(lǐng)域中的研究重點(diǎn)，發(fā)展較快，成果眾多。從理論和分析角度上看，用計(jì)算機(jī)自動證明某一類型幾何定理，一般要經(jīng)歷公理化、坐標(biāo)化與代數(shù)化、機(jī)械化等步驟，就能編制程序并在計(jì)算機(jī)上實(shí)現(xiàn)，條理清晰，用計(jì)算機(jī)進(jìn)行幾何定理證明較易實(shí)現(xiàn)。
現(xiàn)在，幾何定理計(jì)算機(jī)證明的方法主要有以下三種：
一、代數(shù)方法
可用計(jì)算機(jī)證明的幾何定理都假設(shè)坐標(biāo)化與代數(shù)化已經(jīng)完成，而且可把幾何定理的證明問題化為一些代數(shù)關(guān)系式的處理問題，有三種不同類型，與之對應(yīng)則有三種不同的計(jì)算機(jī)證明方法。
第一類，假設(shè)代數(shù)關(guān)系式對于變量是線性的，證明方法為希爾伯特方法；
第二類，假設(shè)代數(shù)關(guān)系式可用多項(xiàng)式的方程表示，證明方法是中國數(shù)學(xué)家吳文俊首先提出的，稱為吳文俊方法，簡稱為吳方法；
第三類，假設(shè)代數(shù)關(guān)系式為多項(xiàng)式等式或不等式，但其系數(shù)必須在一實(shí)閉域中，證明方法為塔斯基方法。
這三種方法各有其適用范圍，但就通用的定理證明來說，希爾伯特法效率較高而塔斯基法效率較低，但前者的適用范圍很窄。
二、幾何不變量消點(diǎn)法
以吳方法為代表的代數(shù)方法僅能夠判斷幾何命題的成立與否，證明過程復(fù)雜，需要進(jìn)行大量的數(shù)值計(jì)算和符號計(jì)算，與傳統(tǒng)幾何證明的簡潔明了相差甚大。人們很難讀懂這種方法生成的證明，因此很多人難以接受這種證明的風(fēng)格。如何生成讓人容易讀懂的幾何證明過程，成為科學(xué)家面臨的又一個(gè)嚴(yán)峻的挑戰(zhàn)。1992年，張景中院士以面積法為基礎(chǔ)，提出了基于幾何不變量的消點(diǎn)法。隨后，他與周咸青、高小山合作完善了這個(gè)方法，利用計(jì)算機(jī)對大量非平凡的幾何命題生成了簡潔易讀的幾何證明。這一杰出的工作被譽(yù)為計(jì)算機(jī)處理幾何問題的里程碑。
三、基于演繹數(shù)據(jù)庫的搜索法
幾何不變量的方法雖然實(shí)現(xiàn)了一大類幾何定理機(jī)器證明的可讀性，但是這種方法得到的證明過程常常不符合人的思維習(xí)慣。而利用演繹數(shù)據(jù)庫的方法，根據(jù)幾何命題所給的條件、已知的公理、定理及公式等推理規(guī)則，通過大量試驗(yàn)匹配的方法進(jìn)行證明，得到從結(jié)論出發(fā)進(jìn)行搜索的后推鏈方法。
隨著幾何定理計(jì)算機(jī)證明的進(jìn)一步發(fā)展，還會有一些新的、更加有效和更易理解的證明方法出現(xiàn)。
數(shù)學(xué)是一棵富有生命力的大樹，從它史前誕生之時(shí)起，就為自己的生存、發(fā)展而斗爭。這場斗爭經(jīng)歷了史前的幾個(gè)世紀(jì)和隨后有文字記載歷史的幾個(gè)世紀(jì)，最后終于在肥沃的希臘土壤中扎穩(wěn)了生存的根基，并且在一個(gè)較短的時(shí)期里茁壯成長起來了。在這個(gè)時(shí)期，它綻出了一朵美麗之花——?dú)W氏幾何。其他的花蕾也含苞欲放。
歐幾里德與《幾何原本》
歐氏幾何是數(shù)學(xué)中最古老的一個(gè)分支，也是數(shù)學(xué)中最基礎(chǔ)的一個(gè)分支。歐氏幾何經(jīng)過了數(shù)千年的發(fā)展和積累，到了公元前三百年左右時(shí)，希臘大數(shù)學(xué)家歐幾里德（Euclid，公元前300年前后）把零散、孤立、不系統(tǒng)的幾何知識總結(jié)成一門具有比較嚴(yán)密理論體系的幾何學(xué)，寫出了數(shù)學(xué)巨著《幾何原本》。
《幾何原本》的偉大歷史意義在于它用公理法建立起最早的數(shù)學(xué)演繹體系，在這個(gè)體系中有四方面的主要內(nèi)容：定義、公理、命題、定理。在這部著作里，全部幾何知識都是從最初的幾個(gè)公理、運(yùn)用邏輯推理的方法展開和敘述的。這些公理、公設(shè)就是《幾何原本》全書的基礎(chǔ)。全書以這些公理和定義為依據(jù)，邏輯地展開它的各個(gè)部分。比如后面出現(xiàn)的每一個(gè)定理都寫明什么是已知、什么是求證，都要根據(jù)前面的定義、公理、定理進(jìn)行邏輯推理給予仔細(xì)證明。
從歐幾里得發(fā)表《幾何原本》到現(xiàn)在已有兩千多年，盡管科學(xué)技術(shù)日新月異，但歐氏幾何仍舊是中學(xué)生學(xué)習(xí)數(shù)學(xué)基礎(chǔ)知識的好教材。長期以來，人們都認(rèn)為《幾何原本》是兩千多年來傳播幾何知識的標(biāo)準(zhǔn)教科書，在西方是除了《圣經(jīng)》以外銷路最廣的一本書。由于歐氏幾何具有鮮明的直觀性并和邏輯演繹方法密切相結(jié)合等特點(diǎn)，長期實(shí)踐表明，它是培養(yǎng)、提高青少年邏輯思維能力的好教材，很多家長以此訓(xùn)練孩子的推理能力。歷史上不知有多少科學(xué)家從歐氏幾何學(xué)習(xí)中得到培養(yǎng)和訓(xùn)練，從而提高了科學(xué)研究的興趣和能力及基礎(chǔ)素質(zhì)，為人類作出了偉大的貢獻(xiàn)。此外，歐氏幾何還具有高超的美學(xué)價(jià)值，隨著幾何學(xué)美妙結(jié)構(gòu)和精確推理的發(fā)展，數(shù)學(xué)變成了一門藝術(shù)。
9. 幾何定理計(jì)算機(jī)證明的方法
從數(shù)學(xué)眾多分支角度上看，幾何在數(shù)學(xué)中歷史地位突出，在數(shù)學(xué)教育中的作用重要，因此對幾何定理進(jìn)行計(jì)算機(jī)證明成了數(shù)學(xué)定理證明領(lǐng)域中的研究重點(diǎn)，發(fā)展較快，成果眾多。從理論和分析角度上看，用計(jì)算機(jī)自動證明某一類型幾何定理，一般要經(jīng)歷公理化、坐標(biāo)化與代數(shù)化、機(jī)械化等步驟，就能編制程序并在計(jì)算機(jī)上實(shí)現(xiàn)，條理清晰，用計(jì)算機(jī)進(jìn)行幾何定理證明較易實(shí)現(xiàn)。
現(xiàn)在，幾何定理計(jì)算機(jī)證明的方法主要有以下三種：
一、代數(shù)方法
可用計(jì)算機(jī)證明的幾何定理都假設(shè)坐標(biāo)化與代數(shù)化已經(jīng)完成，而且可把幾何定理的證明問題化為一些代數(shù)關(guān)系式的處理問題，有三種不同類型，與之對應(yīng)則有三種不同的計(jì)算機(jī)證明方法。
第一類，假設(shè)代數(shù)關(guān)系式對于變量是線性的，證明方法為希爾伯特方法；
第二類，假設(shè)代數(shù)關(guān)系式可用多項(xiàng)式的方程表示，證明方法是中國數(shù)學(xué)家吳文俊首先提出的，稱為吳文俊方法，簡稱為吳方法；
第三類，假設(shè)代數(shù)關(guān)系式為多項(xiàng)式等式或不等式，但其系數(shù)必須在一實(shí)閉域中，證明方法為塔斯基方法。
這三種方法各有其適用范圍，但就通用的定理證明來說，希爾伯特法效率較高而塔斯基法效率較低，但前者的適用范圍很窄。
二、幾何不變量消點(diǎn)法
以吳方法為代表的代數(shù)方法僅能夠判斷幾何命題的成立與否，證明過程復(fù)雜，需要進(jìn)行大量的數(shù)值計(jì)算和符號計(jì)算，與傳統(tǒng)幾何證明的簡潔明了相差甚大。人們很難讀懂這種方法生成的證明，因此很多人難以接受這種證明的風(fēng)格。如何生成讓人容易讀懂的幾何證明過程，成為科學(xué)家面臨的又一個(gè)嚴(yán)峻的挑戰(zhàn)。1992年，張景中院士以面積法為基礎(chǔ)，提出了基于幾何不變量的消點(diǎn)法。隨后，他與周咸青、高小山合作完善了這個(gè)方法，利用計(jì)算機(jī)對大量非平凡的幾何命題生成了簡潔易讀的幾何證明。這一杰出的工作被譽(yù)為計(jì)算機(jī)處理幾何問題的里程碑。
三、基于演繹數(shù)據(jù)庫的搜索法
幾何不變量的方法雖然實(shí)現(xiàn)了一大類幾何定理機(jī)器證明的可讀性，但是這種方法得到的證明過程常常不符合人的思維習(xí)慣。而利用演繹數(shù)據(jù)庫的方法，根據(jù)幾何命題所給的條件、已知的公理、定理及公式等推理規(guī)則，通過大量試驗(yàn)匹配的方法進(jìn)行證明，得到從結(jié)論出發(fā)進(jìn)行搜索的后推鏈方法。
隨著幾何定理計(jì)算機(jī)證明的進(jìn)一步發(fā)展，還會有一些新的、更加有效和更易理解的證明方法出現(xiàn)。