數(shù)學(xué)之十五---初等幾何定理的計(jì)算機(jī)證明

1、數(shù)學(xué)實(shí)驗(yàn)之十五---初等幾何定理的計(jì)算機(jī)證明,中國(guó)科學(xué)技術(shù)大學(xué)數(shù)學(xué)系陳發(fā)來(lái),主要內(nèi)容,符號(hào)計(jì)算與自動(dòng)推理幾何問(wèn)題代數(shù)化代數(shù)關(guān)系式的推導(dǎo)與驗(yàn)證自動(dòng)推理,1、符號(hào)計(jì)算與自動(dòng)推理,符號(hào)計(jì)算 精確的、帶未知變?cè)?、公式的推?dǎo)與驗(yàn)證。 符號(hào)運(yùn)算 自動(dòng)推理自動(dòng)推理 從已知條件推導(dǎo)出結(jié)果，即計(jì)算機(jī)自動(dòng)證明定理、或推導(dǎo)出新的未知的結(jié)論。,,數(shù)學(xué)定理的機(jī)器證明 把一

2、類(lèi)定理作為一個(gè)整體加以考慮，建立一個(gè)統(tǒng)一的、確定的證明程序，對(duì)該類(lèi)定理中的每一個(gè)定理，應(yīng)用證明程序進(jìn)行有限步推理之后即可從命題的假設(shè)推出命題的結(jié)論。 計(jì)算機(jī)自動(dòng)推理實(shí)例 計(jì)算機(jī)象棋、四色定理、初等幾何定理 的計(jì)算機(jī)證明,2、幾何問(wèn)題代數(shù)化,解析幾何是基礎(chǔ) 笛卡兒名言： 一切問(wèn)題都可以化為數(shù)學(xué)問(wèn)題 一切數(shù)學(xué)問(wèn)題都可以化為代數(shù)問(wèn)題 一切代數(shù)問(wèn)題都可以化為方程求解,點(diǎn)

3、 坐標(biāo)線(xiàn) 方程幾何圖形 方程組幾何關(guān)系 方程組條件 方程組結(jié)論 方程組,,,,,,,例 1 證明平行四邊形兩對(duì)角線(xiàn)相互平分,,,,,,,,B,A,C,D,,,N,建立直角坐標(biāo)系如圖。A,B,C的坐標(biāo)如下,其中 為自由參數(shù)。再設(shè)D,N的坐標(biāo)為

4、 ， 則 可以由 所表示。 利用條件AB//CD, AC//BD，可得,于是,利用條件（1），條件（2）可以簡(jiǎn)化為,再由A,N,D共線(xiàn)，B,N,C共線(xiàn)有,由此，,至此，定理的條件化為（1）--（4）。由AN=ND,BN=NC,定理的結(jié)論化為,例 2 證明三角形三邊上的垂線(xiàn)交于一點(diǎn)。,,,,,,,A,B,C,D,E,F,G,建立坐標(biāo)

5、系如圖。設(shè),由B,D,C共線(xiàn)及AD與BC垂直有,因此，,同理，由A,E,C共線(xiàn)及BE與AC垂直有,再由A,G,D與B,G,E分別共線(xiàn)有,結(jié)論：,兩個(gè)問(wèn)題：1、方程與給定的條件與結(jié)論是否等價(jià)？2、如何由給定的一組方程推出另外一 組方程成立？下面以例1為例來(lái)說(shuō)明問(wèn)題1。 在條件： 下等價(jià)。,3、代數(shù)關(guān)系式的推導(dǎo)與驗(yàn)證,給定多項(xiàng)式方程組：,其中 為參數(shù)。如何從上述方程組推

6、導(dǎo)出,思路：尋找函數(shù)i=1,…,n, 使得則由（I）可以推出（II）。吳方法可以實(shí)現(xiàn)上述過(guò)程。,吳方法的步驟：1、將方程組（I）化為三角型方程組：,2、計(jì)算 g 對(duì) 整除所得的余式：,其中 表示以 為主變?cè)?被 整除所得到的偽余式。3、如果 ，則在某些條件下，可以從（I） 推導(dǎo)出 (II)。,偽

7、除法：給定兩個(gè)多項(xiàng)式,其中 是關(guān)于 的多項(xiàng)式，且 。 以 做主變?cè)龆囗?xiàng)式除法其中 是有理式，分母都是 的某個(gè)次冪（設(shè)為 s）。用 同乘上式兩邊,這里 是關(guān)于 的多項(xiàng)式。 稱(chēng)為f 被 g 整除的偽余式。例如，對(duì)于,因此,吳方法

8、的實(shí)現(xiàn)第一步：消元。通過(guò)偽除法實(shí)現(xiàn)。例如，從下列方程組中消去,第二步：逐次偽除法。,從上式得其中 為多項(xiàng)式。,如果 ，則在條件下，由 （I）可以推出 （II）。例 1（續(xù)）：我們要從方程組(1)—(4)推出（5）與（6）。為此，先三角化方程組(1)—(4).,由此，（5）在條件 下成立。,4、自動(dòng)推理,由一些變量之間的已知關(guān)系推