蘇賀靚 江建國(guó) 高 華

（遼寧師范大學(xué)數(shù)學(xué)學(xué)院，遼寧 大連 116029）

0 引言

幾何定理機(jī)器證明是自動(dòng)推理領(lǐng)域內(nèi)的一個(gè)熱門課題.1977年,吳文俊先生提出的“吳法”[1-4]使得幾何定理機(jī)器證明的研究取得了重大進(jìn)展.通常,幾何定理機(jī)器證明方法可分為三大類：代數(shù)法,人工智能法和幾何不變量法.代數(shù)法的優(yōu)點(diǎn)是證明效率高,缺點(diǎn)是可讀性差；人工智能法雖然可讀性好但效率低、不完備；幾何不變量法的可讀性介于代數(shù)法和人工智能法之間,證明效率與代數(shù)法也在伯仲之間.

質(zhì)點(diǎn)幾何使用了比幾何不變量更抽象的對(duì)象——質(zhì)點(diǎn),作為基本幾何元素.莫紹揆先生在文獻(xiàn)[5]中系統(tǒng)地闡述了質(zhì)點(diǎn)幾何的理論和方法.質(zhì)點(diǎn)幾何支持對(duì)點(diǎn)直接進(jìn)行線性運(yùn)算,在處理仿射幾何問(wèn)題時(shí)較方便,為發(fā)展出一種可讀性更好、效率更高的幾何定理機(jī)器證明方法提供了可操作的依據(jù).

鄒宇等人采用質(zhì)點(diǎn)幾何作為模型,在質(zhì)點(diǎn)幾何的基礎(chǔ)上,通過(guò)調(diào)用函數(shù)搜索質(zhì)點(diǎn)在點(diǎn)表中的位置,從而調(diào)用向量表中相應(yīng)位置數(shù)組進(jìn)行運(yùn)算,建立了能處理希爾伯特交點(diǎn)類命題的仿射幾何機(jī)器證明算法MPM,發(fā)展了基于幾何點(diǎn)的可讀機(jī)器證明方法[6-7].

本文是在參考文獻(xiàn)[6]的工作基礎(chǔ)上,針對(duì)其只是對(duì)質(zhì)點(diǎn)所一一對(duì)應(yīng)的數(shù)組做運(yùn)算而非質(zhì)點(diǎn)本身消點(diǎn)運(yùn)算的問(wèn)題,作了純質(zhì)點(diǎn)代數(shù)運(yùn)算.消點(diǎn)過(guò)程比鄒宇的數(shù)組法簡(jiǎn)明.每一步消點(diǎn)過(guò)程都有相應(yīng)的質(zhì)點(diǎn)關(guān)系式輸出,每個(gè)質(zhì)點(diǎn)關(guān)系式又對(duì)應(yīng)于相應(yīng)的幾何信息,消點(diǎn)過(guò)程結(jié)束,質(zhì)點(diǎn)關(guān)系也就都明確了,再利用待定系數(shù)法而非數(shù)組計(jì)算法來(lái)判定結(jié)論語(yǔ)句是否成立,使得每一個(gè)步驟的幾何意義都非常明確.建立了能處理構(gòu)造型幾何定理的證明器MMP,并通過(guò)Matlab語(yǔ)言實(shí)現(xiàn)機(jī)器證明.

1 質(zhì)點(diǎn)幾何

1.1 預(yù)備知識(shí)

質(zhì)點(diǎn)幾何使用了質(zhì)點(diǎn)作為基本的幾何元素.莫紹揆先生在《質(zhì)點(diǎn)幾何學(xué)》一書中系統(tǒng)地闡述了質(zhì)點(diǎn)幾何的理論和方法.質(zhì)點(diǎn)幾何支持對(duì)點(diǎn)直接進(jìn)行線性運(yùn)算,在處理仿射幾何問(wèn)題時(shí)較方便,為發(fā)展出可讀性更好、效率更高的幾何定理機(jī)器證明方法提供了依據(jù).

質(zhì)點(diǎn)是一個(gè)既有位置又有質(zhì)量的基本幾何元素,其質(zhì)量為一個(gè)實(shí)數(shù),可正可負(fù)以及零.質(zhì)點(diǎn)幾何的創(chuàng)新之處在于質(zhì)點(diǎn)均有質(zhì)量.當(dāng)質(zhì)量為非零實(shí)數(shù)時(shí),質(zhì)點(diǎn)表示一個(gè)點(diǎn),或者其對(duì)應(yīng)的位置；當(dāng)質(zhì)量為零時(shí),質(zhì)點(diǎn)表示一個(gè)矢量,或者其對(duì)應(yīng)的方向.

通常,用小寫希臘字母 ω,ξ,ψ,…表示質(zhì)點(diǎn),用大寫英文字母 A,B,C,…表示平面上的點(diǎn),用小寫英文字母a,b,c,…表示實(shí)數(shù),將位于點(diǎn)P處質(zhì)量為m（m≠0）的質(zhì)點(diǎn)記作mP.在不引起混淆的情況下,將位于點(diǎn)P質(zhì)量為1的單位質(zhì)點(diǎn)1P也簡(jiǎn)記成P.質(zhì)點(diǎn)幾何中常用的基本定理和運(yùn)算律主要有：

1）實(shí)數(shù)r與質(zhì)點(diǎn)ω的數(shù)乘決定唯一質(zhì)點(diǎn)rω.

2）兩質(zhì)點(diǎn) ω1,ω2的和決定唯一質(zhì)點(diǎn) ω1+ω2.

3）若P1,P2,P3是質(zhì)點(diǎn)平面的一組基,則該平面上的任一點(diǎn)P都可以由這組基點(diǎn)線性表示,即必存在3個(gè)和為1的實(shí)數(shù)k1,k2和k3,使得P=4）點(diǎn)P在直線AB上當(dāng)且僅當(dāng)存在一個(gè)實(shí)數(shù)k使得P=kA+(1-k)B.5）A,B,C三點(diǎn)共線當(dāng)且僅當(dāng)存在實(shí)數(shù)m和n,使得mA+nB+(1-mn)C=0.

6）直線AB平行直線CD當(dāng)且僅當(dāng)存在一個(gè)實(shí)數(shù)k使得A-B=k(C-D).

7）對(duì)任意質(zhì)點(diǎn)ω1,ω2和ω3,任意實(shí)數(shù)a和b,有如下運(yùn)算律：

1.2 構(gòu)造型質(zhì)點(diǎn)幾何命題

質(zhì)點(diǎn)法不是利用尺規(guī)作要證定理的幾何圖形,而是使用一種叫做“構(gòu)圖語(yǔ)句”作圖步驟按題中的已知條件一步一步地向圖中引入新點(diǎn),直到作出幾何圖形中全部的點(diǎn)為止.

構(gòu)造型幾何命題的前提能用有限的構(gòu)圖語(yǔ)句序列C0,C1,…,Cn描述,這里的構(gòu)圖語(yǔ)句C0必須是初始構(gòu)圖語(yǔ)句,其他構(gòu)圖語(yǔ)句即后繼構(gòu)圖語(yǔ)句中出現(xiàn)的質(zhì)點(diǎn),除了新引進(jìn)的質(zhì)點(diǎn)外,其余的都必須是前面的構(gòu)圖語(yǔ)句所引進(jìn)過(guò)的質(zhì)點(diǎn).

質(zhì)點(diǎn)法使用引入點(diǎn)的“構(gòu)圖語(yǔ)句”來(lái)描述要證定理的前提,本文主要構(gòu)圖語(yǔ)句有以下幾條：

2 證明器的設(shè)計(jì)

2.1 證明器的架構(gòu)

MMP證明器主要由模塊Mmprove、Loadgs和 Cinter組成.

當(dāng)要利用該證明器證明幾何定理時(shí),首先將要證明的幾何命題轉(zhuǎn)化成相應(yīng)的構(gòu)圖語(yǔ)句存儲(chǔ)在文本文件中,Matlab通過(guò)調(diào)用模塊Mmprove中的Loadgs讀取該文本文件,并利用模塊Loadgs將構(gòu)圖語(yǔ)句轉(zhuǎn)化成相應(yīng)的消點(diǎn)公式,來(lái)實(shí)現(xiàn)消點(diǎn)過(guò)程,其中求兩直線交點(diǎn)的消點(diǎn)公式還需要交點(diǎn)模塊Cinter的輔助,依據(jù)質(zhì)點(diǎn)幾何的基本原理和法則完成證明器的實(shí)現(xiàn).

2.2 Loadgs模塊

2.2.1 幾何命題的輸入

證明器MMP的模塊Mmprove順次閱讀構(gòu)圖語(yǔ)句,調(diào)用相應(yīng)的消點(diǎn)公式生成,顯示質(zhì)點(diǎn)關(guān)系式,幾何定理結(jié)論以結(jié)論等式的形式輸出

Loadgs模塊將文本文件中的含有待定系數(shù)x的結(jié)論質(zhì)點(diǎn)等式（EQ標(biāo)識(shí)所在的行）讀入到符號(hào)變量eq中,將要驗(yàn)證的待定系數(shù)的值（XV標(biāo)識(shí)所在的行）讀入到符號(hào)變量xv中.xv的取值為“exit”,表示xv的值只要存在就可以.若xv的值是數(shù)或符號(hào)表達(dá)式,則表示結(jié)論質(zhì)點(diǎn)等式中的待定系數(shù)取此值才成立,否則不成立.

Loadgs模塊將初始構(gòu)圖語(yǔ)句FreePo int s(A,B,C)引入的3個(gè)點(diǎn)A、B和C存儲(chǔ)到基點(diǎn)列表base.構(gòu)圖語(yǔ)句序列中的其它后續(xù)語(yǔ)句所引入的點(diǎn)都可直接或間接地用前面已引入的點(diǎn)線性表示出來(lái).將這些質(zhì)點(diǎn)關(guān)系式稱為構(gòu)圖語(yǔ)句所引入點(diǎn)的消點(diǎn)公式.Loadgs模塊根據(jù)質(zhì)點(diǎn)幾何中的有相關(guān)的基本命題,可以直接求出下列構(gòu)圖語(yǔ)句所引入點(diǎn)的消點(diǎn)公式：

DPDP(X,A,B,λ)所引入點(diǎn)X的消點(diǎn)公式：

Translation(X,A,B,C)所引入點(diǎn)X的消點(diǎn)公式：

上述消點(diǎn)公式中的a和b都是表示實(shí)數(shù)的符號(hào)變量,λ是實(shí)數(shù)或?yàn)楸硎緦?shí)數(shù)的符號(hào)變量,X1,X2和X3是質(zhì)點(diǎn)平面的一組基點(diǎn).

2.2.2 消點(diǎn)公式

在質(zhì)點(diǎn)平面上任作三個(gè)線性無(wú)關(guān)的單位質(zhì)點(diǎn)X,Y和Z.將這三個(gè)單位質(zhì)點(diǎn)選定為其所在的質(zhì)點(diǎn)平面的一組基后,那么構(gòu)圖語(yǔ)句序列中的其它語(yǔ)句所作的點(diǎn)都可直接或間接地用這組基線性表示出來(lái),

這些質(zhì)點(diǎn)公式分別叫做構(gòu)圖語(yǔ)句所作點(diǎn)X的消點(diǎn)公式.具體情況如下：

這里,a和b都是取值為實(shí)數(shù)的符號(hào)變量,λ、u0和v0是取值為實(shí)數(shù)的符號(hào)常量,這些值決定了點(diǎn)X在平面上的確切位置.

2.3 Cinter模塊

在上述消點(diǎn)公式中只有消點(diǎn)公式(epf6)需要復(fù)雜計(jì)算得到.下面給出求消點(diǎn)公式(epf6)的Cinter模塊,該模塊使用前面構(gòu)圖語(yǔ)句所作點(diǎn)的消點(diǎn)公式列表epfs和3個(gè)基點(diǎn),求兩直線AB和CD交點(diǎn)X的消點(diǎn)公式(epf6)中的u0和v0.

將消點(diǎn)公式列表epfs中新引進(jìn)的質(zhì)點(diǎn)Xi(i=1,…,n)依次存儲(chǔ)到初始值為空的元胞數(shù)組po int s中,建立方程eq=uA+(1-u)B-vC-(1-v)D.依次檢驗(yàn)元胞數(shù)組po int s中質(zhì)點(diǎn)Xi(i=1,…,n)是否為eq中的符號(hào)常量,若Xj是的話,則用對(duì)應(yīng)的消點(diǎn)公式epfsj替換掉Xj,繼續(xù)循環(huán),直至eq沒有質(zhì)點(diǎn)Xi(i=1,…,n)出現(xiàn),此時(shí)eq只由基點(diǎn)的關(guān)系式表示.設(shè)基點(diǎn)對(duì)應(yīng)系數(shù)分別用E1,E2和E3表示,令Ei=0(i=1,2,3),解此方程組得u0和v0的值.

3 Matlab實(shí)驗(yàn)

我們用Matlab編寫程序?qū)崿F(xiàn)了MMP證明器,下面是利用該證明器解題的例子.

（高斯線定理）設(shè)A、B、C、D是平面上的四點(diǎn),E是AB、CD的交點(diǎn),F 是 AC、BD 的交點(diǎn),P、Q、R 分別是 AD、BC、EF 的中點(diǎn),則 P、Q、R 三點(diǎn)共線.

在文本文件中輸入：

下面是Matlab程序給出的實(shí)現(xiàn)過(guò)程：

消點(diǎn)過(guò)程：

消點(diǎn)結(jié)束后,令EQ=0,寫成f1(x)A+f2(x)B+f3(x)C=0形式.

這里,系數(shù)fi(a,b)都是a和b的線性表達(dá)式,其中i=1,2,3.因A,B和C線性無(wú)關(guān),可得

這是一個(gè)含有3個(gè)一元一次方程的超定線性方程組,由所作幾何圖形的合理性可知該方程組的解是存在的.解一元一次方程f1(x)=0,求出其解,分別帶入方程f2(x)=0和f3(x)=0中,經(jīng)驗(yàn)算f2(x0)=0和f3(x0)=0成立,則原方程組有且僅有唯一解.

待定系數(shù)x值存在,P,Q,R三點(diǎn)共線.

4 結(jié)論

本文在質(zhì)點(diǎn)幾何基本定理和法則的基礎(chǔ)上,總結(jié)歸納質(zhì)點(diǎn)法解題的特點(diǎn),建立了能處理仿射幾何定理機(jī)器證明的消點(diǎn)過(guò)程,并利用待定系數(shù)的方法而非數(shù)組計(jì)算法來(lái)判定定理結(jié)論是否成立,使得每一個(gè)質(zhì)點(diǎn)關(guān)系式的幾何意義都非常明確．本文基于質(zhì)點(diǎn)法處理幾何點(diǎn)本身,易于擴(kuò)展和融合,形成了具有完全性的消點(diǎn)過(guò)程．由于可以對(duì)點(diǎn)直接進(jìn)行運(yùn)算,質(zhì)點(diǎn)法的消點(diǎn)過(guò)程比面積法或向量法簡(jiǎn)明,并通過(guò)Matlab程序?qū)崿F(xiàn).

本文的質(zhì)點(diǎn)法是繼面積法之后又一個(gè)能對(duì)構(gòu)造性幾何命題生成可讀證明的完全的消點(diǎn)過(guò)程．運(yùn)行結(jié)果顯示,本文的方法不僅效率高,程序自動(dòng)生成的證明條理簡(jiǎn)明清晰、語(yǔ)義簡(jiǎn)潔易懂、幾何意義明確、儲(chǔ)存信息豐富,可讀性強(qiáng)．此外,由于可以對(duì)點(diǎn)直接進(jìn)行運(yùn)算,質(zhì)點(diǎn)法的算法和編程比面積法或向量法都要簡(jiǎn)明.本文基于點(diǎn)的可讀機(jī)器證明的研究為擴(kuò)展和融合其他已有的可讀證明方法提供了基礎(chǔ),也為幾何的研究提供了一個(gè)新的工具．

隨著計(jì)算機(jī)技術(shù)的發(fā)展和機(jī)器證明方法的不斷改進(jìn),幾何定理可讀證明的研究成果為研制的智能幾何軟件如幾何專家、超級(jí)畫板等提供了更廣闊的平臺(tái).

［1］吳文俊.初等幾何判定問(wèn)題與機(jī)械化證明[J].中國(guó)科學(xué)(A),1977,6：507-516.

［2］Wu W T.On the decision problem and the mechanization of theorem-proving in elementary geometry[J].Scientia Sinica.1978,21：159-172.

［3］Wu W T.Mechanical theorem proving in geometries：Basic principles[M].Springer,New York,1994.

［4］Wu W T.Mathematics Mechanization[M].Science Press,Kluwer,2000.

［5］莫紹揆.質(zhì)點(diǎn)幾何學(xué)[M]．重慶：重慶出版社,1992.

［6］鄒宇.幾何代數(shù)基礎(chǔ)與質(zhì)點(diǎn)幾何的可讀機(jī)器證明[D].廣州：廣州大學(xué),2010.

［7］鄒宇,鄭煥,張景中.仿射質(zhì)點(diǎn)幾何的可讀機(jī)器證明[J].計(jì)算機(jī)應(yīng)用,2010,30(7)：1989-1912.