質點幾何定理證明的機器實現(xiàn)

蘇賀靚 江建國 高 華

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

0 引言

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

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

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

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

1 質點幾何

1.1 預備知識

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

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

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

1）實數(shù)r與質點ω的數(shù)乘決定唯一質點rω.

2）兩質點 ω1,ω2的和決定唯一質點 ω1+ω2.

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

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

7）對任意質點ω1,ω2和ω3,任意實數(shù)a和b,有如下運算律：

1.2 構造型質點幾何命題

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

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

質點法使用引入點的“構圖語句”來描述要證定理的前提,本文主要構圖語句有以下幾條：

2 證明器的設計

2.1 證明器的架構

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

當要利用該證明器證明幾何定理時,首先將要證明的幾何命題轉化成相應的構圖語句存儲在文本文件中,Matlab通過調用模塊Mmprove中的Loadgs讀取該文本文件,并利用模塊Loadgs將構圖語句轉化成相應的消點公式,來實現(xiàn)消點過程,其中求兩直線交點的消點公式還需要交點模塊Cinter的輔助,依據(jù)質點幾何的基本原理和法則完成證明器的實現(xiàn).

2.2 Loadgs模塊

2.2.1 幾何命題的輸入

證明器MMP的模塊Mmprove順次閱讀構圖語句,調用相應的消點公式生成,顯示質點關系式,幾何定理結論以結論等式的形式輸出

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

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

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

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

上述消點公式中的a和b都是表示實數(shù)的符號變量,λ是實數(shù)或為表示實數(shù)的符號變量,X1,X2和X3是質點平面的一組基點.

2.2.2 消點公式

在質點平面上任作三個線性無關的單位質點X,Y和Z.將這三個單位質點選定為其所在的質點平面的一組基后,那么構圖語句序列中的其它語句所作的點都可直接或間接地用這組基線性表示出來,

這些質點公式分別叫做構圖語句所作點X的消點公式.具體情況如下：

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

2.3 Cinter模塊

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

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

3 Matlab實驗

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

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

在文本文件中輸入：

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

消點過程：

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

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

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

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

4 結論

本文在質點幾何基本定理和法則的基礎上,總結歸納質點法解題的特點,建立了能處理仿射幾何定理機器證明的消點過程,并利用待定系數(shù)的方法而非數(shù)組計算法來判定定理結論是否成立,使得每一個質點關系式的幾何意義都非常明確．本文基于質點法處理幾何點本身,易于擴展和融合,形成了具有完全性的消點過程．由于可以對點直接進行運算,質點法的消點過程比面積法或向量法簡明,并通過Matlab程序實現(xiàn).

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

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

［1］吳文俊.初等幾何判定問題與機械化證明[J].中國科學(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］莫紹揆.質點幾何學[M]．重慶：重慶出版社,1992.

［6］鄒宇.幾何代數(shù)基礎與質點幾何的可讀機器證明[D].廣州：廣州大學,2010.

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