人教版高中數學必修二《閱讀與思考-坐標法與機器證明》

坐標法與機器證明閱讀與思考笛卡爾的設想一切問題化為數學問題，一切數學問題化為代數問題一切代數問題化為代數方程求解問題。笛卡爾解析幾何之父意味著幾何定理機械化證明成為了一種

可能。幾何問題

的求解或

求證問題空間形式的

推理問題代數方程的

求解問題計算問題笛卡爾創(chuàng)立坐標系數學機械化數學問題的機械化----在運算或證明

的過程中，每前進一步之后，都有一

個確定的，必須選擇的下一步，這樣

沿著一條有規(guī)律、刻板的道路，

一直

到達結論。他明確的提出機器可以成為推理工具的思想，由

于當時的條件限制，計算僅僅是手工操作(手搖

計算機),無法進行大量復雜的計算，所以用機

器實現幾何定理證明的想法無法實現。數學機械化：從設想到實現萊布尼茲幾何定理機器證明---

“吳方法”他將幾何定理證明從一個不太成功的領域，變?yōu)橐粋€最成功的領域。數學機械化：從設想到實現吳文俊吳文俊機器證明的思想吳文俊機器證明的思想主要是從笛卡爾的坐標法和中國古代解方程的

計算方法而來，把空間形式的推理轉

化成數量關系來處理?！皡欠椒ā弊C明幾何定理是基于什么樣的原理去實現的呢?條件：四邊形ABCD結論：

AC⊥BD例證明：菱形的對角線互相垂直。是菱形幾何畫板A(0,0)其中u,u,是與幾何命題的假設條件無關的自由變是參數)

,x,x?

是受幾何條件限制的約束變元。幾何問題代數化---選取合適坐標代數化f?=x(u?-u?)=x,x?=0f?=u2-(x2+x?2)=0代數化條件AD//BC:AB=AD:結論AC

⊥BD:第

一

步

：

將

已

知

條

件

和

結

論

代

數

化第二步：將已知條件多項式整序(三角化)條件多項式整理f=u?-u?=x?=0f?=u2-(x2+x?2)=0目標多項式證明：g=x2+u?

(x?-u?)=0分析：

g

=

·f?+

·f?66

分

析

：g=x2+u?

(x?-u?)g=-f?+u2=x?2+u?(x?-u?)g=-f?+(u?-x?)(u?+x?)+u?(x?-u?)g=-f?+(x?-u?)(u?-u?-x?)g=-f?+(x?-u?)f又∵f=0,f?=0∴g=0,

即定理被證明吳方法”原理第三步：做逐步除法(1)將g除以f?(以x

為未知量)得余式r?

-

-x?2+u?(x?-u?)∴I5=u2-x?2+u?(x?=u?)(2)將余式r?除以f

(以x?為未知量)得余式r(即r?=Gfi+)即g=-f?+(x?-u?)f因此必有g=0,

故定理得證r(即gf?g?f∵r?=(x?-u?)f

∴I=0“吳方法”證明幾何基本定理的一般步驟第一步：將幾何定理條件代數化定理的結論代數化：

第二步：將條件多項式整序(三角化)第三步：做逐步除法(1)將g除以f

(以x,為未知量)得余式即g=Cmfm+rm

(其中cm為非0的商)(2)將余式r;除以，(以x

為未知量)得余式m即m=Cmf+r

(其中cm

為非0的商)如此繼續(xù)進行下去，直到最后的余式，若r=0,

則定理得證。上述步驟在Mathematica軟件中可以自動完成展