1、數學實驗之十五-初等幾何定理的計算機證明中國科學技術大學數學系陳發來主要內容 符號計算與自動推理 幾何問題代數化 代數關系式的推導與驗證 自動推理1、符號計算與自動推理 符號計算 精確的、帶未知變元的、公式的推導與驗證。 符號運算 自動推理 自動推理 從已知條件推導出結果，即計算機自動證明定理、或推導出新的未知的結論。 數學定理的機器證明 把一類定理作為一個整體加以考慮，建立一個統一的、確定的證明程序，對該類定理中的每一個定理，應用證明程序進行有限步推理之后即可從命題的假設推出命題的結論。 計算機自動推理實例 計算機象棋、四色定理、初等幾何定理 的計算機證明2、幾何問題代數化 解析幾何是基礎

2、笛卡兒名言： 一切問題都可以化為數學問題一切問題都可以化為數學問題 一切數學問題都可以化為代數問題一切數學問題都可以化為代數問題 一切代數問題都可以化為方程求解一切代數問題都可以化為方程求解 點 坐標線 方程幾何圖形 方程組幾何關系 方程組條件 方程組結論 方程組例例 1 證明平行四邊形兩對角線相互平分 BACDN建立直角坐標系如圖。A,B,C的坐標如下),(),0 ,(),0 , 0(321uuCuBA其中 為自由參數。再設D,N的坐標為 ， 則 可以由 所表示。 利用條件AB/CD, AC/BD，可得321,uuu),(),(4321xxNxxD4321,xxxx321,uuu231122

3、1320uuuxxuxux于是)2(0)(:)1(0:223112321uxuuxhuxh利用條件（1），條件（2）可以簡化為)2(0:2112uuxh再由A,N,D共線，B,N,C共線有1334xuxx123134uuuuxx由此，)4(0)()(:)3(0:313124433143uuxuuxhuxxxh至此，定理的條件化為（1）-（4）。由AN=ND,BN=NC,定理的結論化為)6(02)(2:)5(022:232221342132224231211uuuuxuuxgxxxxxxg例例 2 證明三角形三邊上的垂線交于一點。ABCDEFG建立坐標系如圖。設)0 ,(),0 ,(21uBuA

4、),(),(),(), 0(6543213xxGxxExxDuC由B,D,C共線及AD與BC垂直有12311223212uuuxxuuuxx因此，)2(0)(:) 1 (0)(:112232213221uxuxuhuxuxuh同理，由A,E,C共線及BE與AC垂直有)4(0)(:)3(0)(:232434133413uxuxuhuxuxuh再由A,G,D與B,G,E分別共線有)6(0)()(:)5(0)()(:11615262362545uxxuxxhuxxuxxh結論：)7(05x兩個問題：1、方程與給定的條件與結論是否等價？2、如何由給定的一組方程推出另外一 組方程成立？下面以例1為例來說

5、明問題1。 在條件： 下等價。031uu3、代數關系式的推導與驗證給定多項式方程組：)(0),.,.,(.0),.,.,(11111Ixxuuhxxuuhnmnnm其中 為參數。如何從上述方程組推導出muu ,.,1)(0),.,.,(11IIxxuugnm思路：尋找函數i=1,n, 使得則由（I）可以推出（II）。吳方法可以實現上述過程。, 0),.,.,(11nmixxuuq)(.,2211IIIhqhqhqgnn吳方法的步驟：1、將方程組（I）化為三角型方程組：)(0),.,.,(.0),.,(11111IVxxuufxuufnmnm2、計算 g 對 整除所得的余式： 1,., ffn)

6、(),(Re.),(Re),(Re111011, 121VxfRmRxfRmRxfgmRnnnnnnn其中 表示以 為主變元， 被 整除所得到的偽余式。3、如果 ，則在某些條件下，可以從（I） 推導出 (II)。),(ReiiixfRmixiRif00R偽除法：給定兩個多項式0101.dydydgcycycfnnmm其中 是關于 的多項式，且 。 以 做主變元做多項式除法其中 是有理式，分母都是 的某個次冪（設為 s）。用 同乘上式兩邊iidc ,nxx ,.,1mn yrgqfrq,ndsndrqgfdsn這里 是關于 的多項式。 稱為f 被 g 整除的偽余式。例如，對于yxxn,.,1rq

7、,),(Reygfmr 2,332yxgyyxf6228),(Rexxygfm62625283328)42()(xxgxxyxyxfx因此吳方法的實現第一步：消元。通過偽除法實現。例如，從下列方程組中消去3212222111xxhxxh2x221121231),(Rexxxxhhmh61211231421),(Rexxxxhhmh第二步：逐次偽除法。)(.0111121111111VIRfqRdRfqRdRfqgdsnnnnsnnnnsnnn從上式得其中 為多項式。)(.01111VIIRfAfAgddnnsnsnnAA ,.,1如果 ，則在條件下，由 （I）可以推出 （II）。例例 1（續）

8、：我們要從方程組(1)(4)推出（5）與（6）。為此，先三角化方程組(1)(4).00R0.21nddd32221121,uxfuuxhf31333213314433)(),(Rexxuxuuxxuuxhhmf31312444)()(uuxuuxhf0)()(:0)(003131244313332133133222111uuxuuxfxxuxuuxxuufuxfuuxf3133123112222122114413222),(RexxuxxuxxuxuxuxuxfgmR)2()(),(Re221222221231312122113213332xxxuxuxuuxxuxuuuuxfRmR)()(),(Re21231213212221xuxuuuuuxfRmR0),(Re1110 xfRmR由此，（5）在條件 下成立。0, 0)(12421133uuIuuxuI4、自動推理 由一些變量之間的已知關系推導一些變量之間的未知關系。 例例 3 推導正五邊形的邊長與連接不相鄰的兩個頂點的線段長度之間的關系。ABCDEOxy以正五邊形中心為坐標原點建立直角坐標系如圖。設 則 由ABCDE為正五邊形有),(),(),(), 0(4242315xxDxxCxxBxA),(31xxE 122| ,2|xBExCD04)(0)()()(0022253214243212253213252422