李曉霞

摘要：如何根據(jù)用戶(hù)輸入的已知條件生成幾何圖形是幾何定理機(jī)器可讀證明過(guò)程中首先要解決的問(wèn)題。針對(duì)幾何定理機(jī)器證明過(guò)程中圖形的生成及動(dòng)態(tài)變換問(wèn)題，結(jié)合幾何命題的構(gòu)造性特點(diǎn)，提出了一種改進(jìn)的幾何約束求解算法，該方法通過(guò)代數(shù)方程組來(lái)表示和處理幾何圖形的約束關(guān)系，并將代數(shù)方程組化簡(jiǎn)為三角列式，通過(guò)對(duì)三角列式的求解來(lái)完成圖形的生成和變換。通過(guò)對(duì)比證明該算法克服了傳統(tǒng)方法的一些缺陷，并能較好地實(shí)現(xiàn)幾何圖形的動(dòng)態(tài)特性。

關(guān)鍵詞：幾何約束關(guān)系； 約束求解； 謂詞語(yǔ)句； 構(gòu)造語(yǔ)句； 三角列

中圖分類(lèi)號(hào)：TP181 文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：2095-2163（2013）06-0088-04

幾何定理機(jī)器證明已有數(shù)十年的探索與發(fā)展，針對(duì)結(jié)論產(chǎn)生的可讀證明也日漸成熟，但人們對(duì)證明過(guò)程的分析與理解還是要依托借助于幾何圖形，而在分析幾何圖形時(shí)，仍然需要經(jīng)常拖動(dòng)圖形中的某些點(diǎn)，然后查看圖形的相應(yīng)變化。因此，如何根據(jù)用戶(hù)輸入的已知條件生成動(dòng)態(tài)幾何圖形，是幾何定理機(jī)器證明中亟待解決的首要問(wèn)題。而幾何圖形是由幾何元素以及這些元素之間的約束關(guān)系所組成的，圖形的生成過(guò)程就是確定幾何元素及其約束關(guān)系的過(guò)程，而且在圖形動(dòng)態(tài)變化時(shí)，還需要保持幾何元素之間的約束關(guān)系依然成立，在本質(zhì)上這是一個(gè)約束求解的過(guò)程[1]。

1傳統(tǒng)的幾何約束求解方法

使用傳統(tǒng)的幾何約束求解算法在解答圖形問(wèn)題時(shí)，首先要根據(jù)給出的已知幾何信息，確定某點(diǎn)P后，遍歷和點(diǎn)P相關(guān)的所有其他點(diǎn)P1，再依據(jù)相應(yīng)的幾何約束關(guān)系生成或更新P1的狀態(tài)。然后，對(duì)點(diǎn)P1進(jìn)行類(lèi)似的操作，如此不斷持續(xù)，直到所有點(diǎn)都得到生成或點(diǎn)的狀態(tài)均實(shí)現(xiàn)了更新。該方法的原理比較簡(jiǎn)單，但算法卻需要進(jìn)行多次的遍歷比較，使得效率不是很高。同時(shí)由于傳統(tǒng)算法未能對(duì)幾何約束關(guān)系采取統(tǒng)一的表示方法，因此很難保證圖形的正確性及完整性，并且對(duì)于許多圖形的退化條件也未能給出正確的結(jié)果[1]。

使用代數(shù)方程來(lái)處理幾何圖形的約束關(guān)系在1948年Tarski就提出了，但由于該方法效率低，并未獲得實(shí)際的應(yīng)用。1977年，吳方法的出現(xiàn)在幾何定理的機(jī)器證明方面取得了巨大的成功，吳方法通過(guò)引進(jìn)坐標(biāo)系，將幾何定理的前提條件（幾何約束）統(tǒng)一表示為代數(shù)方程的形式，定理的證明就等價(jià)于條件的代數(shù)方程能否推出結(jié)論的代數(shù)方程，實(shí)驗(yàn)證明吳方法的證明效率是比較高的[2]。但吳方法主要適用于定理的判定，并不適用于定理的可讀證明，如果用吳方法去直接求解幾何圖形，則可能會(huì)導(dǎo)致求解結(jié)果和用戶(hù)所預(yù)期的結(jié)果相差甚遠(yuǎn)，本文即試圖尋求一種高效的動(dòng)態(tài)圖形生成算法。

2算法思想

受吳方法的啟示，本文將幾何圖形中的約束關(guān)系統(tǒng)一表示為代數(shù)方程組的形式，通過(guò)對(duì)代數(shù)方程組的化簡(jiǎn)、求解來(lái)生成圖形。在將幾何定理的約束條件轉(zhuǎn)化為代數(shù)方程的過(guò)程中，一個(gè)關(guān)鍵步驟就是給定理中的點(diǎn)設(shè)定坐標(biāo)參數(shù)。從理論上來(lái)說(shuō)，點(diǎn)的坐標(biāo)參數(shù)的任意性并不影響定理的有效性。然而參數(shù)選擇不當(dāng)，很容易產(chǎn)生一個(gè)高度耦合的代數(shù)方程組，對(duì)這樣的代數(shù)方程組進(jìn)行化簡(jiǎn)和求解的復(fù)雜度也相應(yīng)會(huì)增加很多。事實(shí)上，大部分的幾何定理都是構(gòu)造型的（可以使用直尺和圓規(guī)作圖生成的），因此，可以將兒何定理轉(zhuǎn)化成構(gòu)造形狀表示，使每條構(gòu)造語(yǔ)句只引進(jìn)一個(gè)新的點(diǎn)，并根據(jù)該構(gòu)造順序依次給點(diǎn)的坐標(biāo)參數(shù)賦值，由此得到一個(gè)依賴(lài)關(guān)系相對(duì)比較簡(jiǎn)單的多項(xiàng)式方程組，再將該方程組局部消解為三角序列的形式，對(duì)該三角序列求解就可以快速地實(shí)現(xiàn)圖形的計(jì)算和變換。

3幾何命題的表示形式

3.1構(gòu)造形式

因此，一個(gè)構(gòu)造型幾何命題可以表示為GS = （C1，C2…Ck，G）。 這里的每條構(gòu)圖語(yǔ)Ci（i=1…k） 都分別引入一個(gè)新的點(diǎn)，且當(dāng)i>j時(shí)，構(gòu)圖語(yǔ)句Ci中所有參數(shù)U都由之前的構(gòu)圖語(yǔ)句Cj引進(jìn)，G是命題結(jié)論。

例如：西門(mén)松定理（令點(diǎn)D是△ABC的外接圓（o）上的任意一點(diǎn)，從D點(diǎn)作三條垂線(xiàn)到三角形三條邊BC，AC和AB，分別交于E、F和G三個(gè)點(diǎn)，證明E、F和G三點(diǎn)共線(xiàn)。）的構(gòu)造形式如下：

3.2謂詞形式

構(gòu)造型幾何命題對(duì)于描述幾何定理的作圖過(guò)程與定理的證明都很方便，但在命題輸入時(shí)，構(gòu)造語(yǔ)句更多地是注重點(diǎn)的順序，而與用戶(hù)平時(shí)看到的“由假設(shè)推得結(jié)論”的過(guò)程并不相符。因此，人們更習(xí)慣輸入前提條件所代表的是幾何圖形中各元素間的約束關(guān)系，并且一般都是以謂詞語(yǔ)句的形式表示的。謂詞形式由點(diǎn)的構(gòu)造序列、假設(shè)條件和結(jié)論構(gòu)成，幾何約束關(guān)系由謂詞表示[4]。

一個(gè)謂詞型的幾何命題可以表述為WS=（Pts，Ps，G）。其中，Pts是命題中的點(diǎn)的序列；Ps是代表命題中各元素間約束關(guān)系的謂詞語(yǔ)句；G是命題的結(jié)論。

謂詞語(yǔ)句在描述幾何命題時(shí)能夠更為直觀(guān)地反映命題的前提條件，但點(diǎn)的構(gòu)造并不嚴(yán)格，若轉(zhuǎn)化成代數(shù)方程組，則對(duì)該方程組的求解就會(huì)比較復(fù)雜，因此，需要將用戶(hù)輸入的謂詞形式轉(zhuǎn)換為構(gòu)造形式。

3.3幾何命題的謂詞形式到構(gòu)造形式的轉(zhuǎn)化算法

根據(jù)謂詞語(yǔ)句中點(diǎn)的序列Pts，可以將幾何命題的謂詞形式轉(zhuǎn)化成構(gòu)造形式，轉(zhuǎn)化算法如下：

（1）從Pts列表中選擇最后的點(diǎn)X（如果Pts為空，則退出），將點(diǎn)X從Pts中移除。

（2）從Ps中選取所有和X相關(guān)的謂詞。由于每個(gè)點(diǎn)至多有兩個(gè)參數(shù)，因此和該點(diǎn)相關(guān)的謂詞可能有0，1或2個(gè)，若超過(guò)兩個(gè)，則認(rèn)為該點(diǎn)是過(guò)約束的，定理無(wú)法構(gòu)造，算法結(jié)束。

（a）如果和點(diǎn)X相關(guān)的謂詞個(gè)數(shù)為0，則該點(diǎn)是一個(gè)自由點(diǎn)，生成構(gòu)造語(yǔ)句（Point p）；

（b）如果和點(diǎn)X相關(guān)的謂詞個(gè)數(shù)為1，則該點(diǎn)是一個(gè)半自由點(diǎn)，生成相應(yīng)的構(gòu)造語(yǔ)句；

（c）如果和點(diǎn)X相關(guān)的謂詞個(gè)數(shù)為2，則該點(diǎn)是一個(gè)約束點(diǎn)，生成相應(yīng)的構(gòu)造語(yǔ)句。

（3）將Ps中所有和點(diǎn)X相關(guān)的謂詞都刪除，返回步驟（1）。

通過(guò)上述算法，當(dāng)Pts為空時(shí)，就可以逐步得到與命題相關(guān)的構(gòu)造語(yǔ)句。

4動(dòng)態(tài)幾何圖形的生成

將幾何命題的約束條件表示為構(gòu)造形式后，即可使用改進(jìn)的幾何約束算法將幾何命題轉(zhuǎn)化為代數(shù)方程組，并對(duì)代數(shù)方程組進(jìn)行化簡(jiǎn)求解，最終生成動(dòng)態(tài)幾何圖形。算法步驟如下：

（1）給幾何命題中的點(diǎn)分配坐標(biāo)參數(shù)

本算法中的幾何命題采用以點(diǎn)為基礎(chǔ)的表示方法，因此只需要關(guān)注幾何定理中點(diǎn)的參數(shù)即可。在笛卡爾坐標(biāo)下，每個(gè)點(diǎn)包含x和y兩個(gè)參數(shù)。 由于構(gòu)造型幾何命題中的點(diǎn)是逐步引進(jìn)的，每個(gè)構(gòu)造語(yǔ)句只引進(jìn)了一個(gè)新點(diǎn)，且構(gòu)造的新點(diǎn)只和之前所構(gòu)造的點(diǎn)彼此相關(guān)。因此，如果根據(jù)構(gòu)造語(yǔ)句中點(diǎn)引進(jìn)的順序依次給點(diǎn)的坐標(biāo)分配參數(shù)，那么這個(gè)點(diǎn)的坐標(biāo)參數(shù)將只依賴(lài)于在該點(diǎn)之前己經(jīng)構(gòu)造出來(lái)的點(diǎn)的參數(shù)，由此產(chǎn)生的多項(xiàng)式方程組中的參數(shù)依賴(lài)關(guān)系將會(huì)變得相對(duì)簡(jiǎn)單[5]。令幾何定理中點(diǎn)的構(gòu)造序列為{P1，P2，…，Pi}，則分配參數(shù)的方式為：Pi =（x2i-1， x2i）

其中，x2i-1 ，x2i對(duì)應(yīng)點(diǎn)Pi的坐標(biāo)參數(shù)x，y，對(duì)于這些參數(shù)變?cè)?，還需要給其規(guī)定順序，假定當(dāng)且僅當(dāng)i

（2）將幾何命題的約束條件轉(zhuǎn)化為代數(shù)方程組

幾何命題的謂詞語(yǔ)句都可以使用代數(shù)方程來(lái)表示，如點(diǎn)A（x1，x2），B（x3，x4），C（x5，x6）共線(xiàn)的謂詞語(yǔ)句為（OnLine A B C），該語(yǔ)句轉(zhuǎn)換成代數(shù)方程的表示形式為（x6-x2）*（x3-x1）-（x5-x1）*（x4-x2）= 0。

在幾何命題的構(gòu)造語(yǔ)句中，除自由點(diǎn)外，每條構(gòu)造語(yǔ)句都是由一條或者兩條謂詞語(yǔ)句產(chǎn)生的，而構(gòu)造語(yǔ)句的代數(shù)方程就是該語(yǔ)句所對(duì)應(yīng)的謂詞語(yǔ)句的代數(shù)方程。若構(gòu)造的點(diǎn)是半自由點(diǎn)，則對(duì)應(yīng)一個(gè)多項(xiàng)式方程，該方程引進(jìn)兩個(gè)新參數(shù)，其它參數(shù)在這兩個(gè)參數(shù)之前引進(jìn)；若構(gòu)造的點(diǎn)是約束點(diǎn)，則對(duì)應(yīng)兩個(gè)多項(xiàng)式方程，且引進(jìn)兩個(gè)新參數(shù)。

令定理的前提條件所對(duì)應(yīng)的多項(xiàng)式集合為HS，不失一般性，總是有：

（3）將代數(shù)方程組化簡(jiǎn)為三角列形式

將一般的代數(shù)多項(xiàng)式方程組化簡(jiǎn)為三角列形式，類(lèi)似于將一個(gè)矩陣轉(zhuǎn)化成下三角形或者上三角形，該過(guò)程并不容易。本算法根據(jù)構(gòu)造語(yǔ)句中點(diǎn)引進(jìn)的順序依次給點(diǎn)的坐標(biāo)賦值，由此產(chǎn)生的多項(xiàng)式方程組中的參數(shù)依賴(lài)關(guān)系則變得相對(duì)簡(jiǎn)單，多項(xiàng)式方程組的耦合度也大大降低，對(duì)其化簡(jiǎn)就會(huì)相對(duì)容易。

對(duì)于一個(gè)半自由點(diǎn)對(duì)應(yīng)的多項(xiàng)式方程，可以把其中的一個(gè)參數(shù)當(dāng)作自由變?cè)硪粋€(gè)參數(shù)則由當(dāng)前的方程引進(jìn)，因此這個(gè)方程不需要化簡(jiǎn)就可以直接求解。而關(guān)于一個(gè)約束點(diǎn)對(duì)應(yīng)兩個(gè)多項(xiàng)式方程，則只需要消掉其中一個(gè)方程當(dāng)中的一個(gè)參數(shù)即可直接求解。因此，構(gòu)造型幾何命題的多項(xiàng)式方程組的三角化就可以局部分塊進(jìn)行。令點(diǎn)P的坐標(biāo)參數(shù)為（xi， xi+1），在這里只需要考慮點(diǎn)P是一個(gè)約束點(diǎn)的情況，令點(diǎn)P的構(gòu)造語(yǔ)句所對(duì)應(yīng)的代數(shù)方程組是：

在三角列中每個(gè)多項(xiàng)式方程只引進(jìn)一個(gè)新的參數(shù)。

（4）對(duì)三角形式的代數(shù)方程組進(jìn)行順序求解，得到當(dāng)前圖形的最新?tīng)顟B(tài)。

在CS中，自由變?cè)猽1，…，ud對(duì)應(yīng)圖形中的自由點(diǎn)，各變?cè)闹凳强梢宰杂蛇x擇的。當(dāng)u1，…，ud的值被確定以后，剩下的變?cè)獂1，…，x2r就可以根據(jù)三角化以后的方程組依次求解。此時(shí)如果拖動(dòng)鼠標(biāo)，使得一個(gè)或者多個(gè)自由變?cè)猽1，…，ud的值發(fā)生變化，那么x1，…，x2r也會(huì)隨之發(fā)生變化，由此即可計(jì)算得到圖形中所有的點(diǎn)坐標(biāo)。該方法使得圖形的基本約束關(guān)系始終成立，而且也可以得到滿(mǎn)意的動(dòng)態(tài)效果。

5算法分析

利用代數(shù)方法處理幾何圖形的約束關(guān)系具有非常重要的意義，因其增強(qiáng)了幾何作圖的能力。通過(guò)在幾何定理機(jī)器證明平臺(tái)中大量的例子證明，該算法避免了傳統(tǒng)約束求解方法的許多問(wèn)題，且具有如下優(yōu)點(diǎn)：

（1）求解效率高

本算法中生成的代數(shù)方程組是逐步引進(jìn)坐標(biāo)點(diǎn)的，且最后三角化的方程組是依次求解的，如此，方程的求解效率就非常高，圖形生成的速度也十分快。

（2）約束求解的過(guò)程穩(wěn)定

本算法中構(gòu)造語(yǔ)句是基于點(diǎn)的，幾何命題可以通過(guò)代數(shù)方程直接利用求根根式計(jì)算得到，因此求解過(guò)程非常穩(wěn)定，且隨意拖動(dòng)圖形中的某個(gè)點(diǎn)時(shí)，不會(huì)產(chǎn)生跳躍現(xiàn)象。

（3）可以構(gòu)造出幾何圖形的多種可能情況

在對(duì)代數(shù)方程組求解的過(guò)程中，對(duì)于四次以及四次以下的代數(shù)方程可以直接運(yùn)用求根根式得到方程所有的解。因此，可以構(gòu)造出幾何圖形的所有可能情況。

（4）重合點(diǎn)的自動(dòng)發(fā)現(xiàn)和去除

在幾何作圖的過(guò)程中，經(jīng)常會(huì)遇到產(chǎn)生重合點(diǎn)的情況。所謂重合點(diǎn)，就是指一個(gè)新作出的點(diǎn)實(shí)際上己經(jīng)被先前的構(gòu)造過(guò)程產(chǎn)生了。在本算法中能夠?qū)缀味ɡ淼那疤釛l件都轉(zhuǎn)化成三角形式的代數(shù)方程組，且每當(dāng)一個(gè)新的點(diǎn)構(gòu)造出來(lái)的時(shí)候，可首先使用數(shù)值檢測(cè)方法，檢查這個(gè)點(diǎn)的坐標(biāo)是否和先前己經(jīng)構(gòu)造的某個(gè)點(diǎn)重合[6]，如果兩者的坐標(biāo)在某個(gè)誤差范圍之內(nèi)，即可判定為重合點(diǎn)，去除該點(diǎn)。

當(dāng)然本算法也存在不足之處，在用戶(hù)輸入的幾何命題前提條件時(shí)， 必須要輸入點(diǎn)的序列， 這就要求用戶(hù)首先對(duì)幾何圖形要有清楚的認(rèn)識(shí)，且命題中涉及到構(gòu)造特定長(zhǎng)度的線(xiàn)段，或特定值的角度，或包含不等式時(shí)，使用該方法就存在困難，這也是今后該研究要努力探索的方向。

參考文獻(xiàn)：

[1]張巖.幾何約束求解的偶圖分解法[D].哈爾濱：黑龍江大學(xué)，2008：46-55.

[2]吳文俊.初等幾何判定問(wèn)題與機(jī)械化證明[J].中國(guó)科學(xué)，1977，（6）50-56.

[3]林強(qiáng)， 高小山. 基于幾何約束求解的完備方法[J].計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)，2007，（7）23-26.

[4]李洪波.幾何定理機(jī)器證明的新探索[D].北京：北京大學(xué)，1994：23-41.

[5]CHOU S C，GAO X S，ZHANG J Z.A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Auto-mated Reasoning，2000，25（3）：219-246.

[6]李傳中，張景中.超級(jí)畫(huà)板[M]. 北京：北京師范大學(xué)出版社，2004.