平面幾何的動(dòng)態(tài)可視證明研究.pdf

1、當(dāng)我們閱讀幾何書本上的證明的時(shí)候，通常需要花費(fèi)相當(dāng)?shù)臅r(shí)間和精力來(lái)辨識(shí)證明文本中的幾何元素和幾何圖形的對(duì)應(yīng)關(guān)系。當(dāng)幾何圖形或者證明變得復(fù)雜的時(shí)候，這個(gè)問(wèn)題就會(huì)變得很嚴(yán)重。因此，如何在計(jì)算機(jī)中重新組織和表示幾何證明使得它們更容易閱讀和理解將是一件十分有意義的事情，這也是證明可視化研究的主要課題之一。
　　 本文對(duì)平面幾何證明可視化方面目前存在的問(wèn)題進(jìn)行了深入的研究，其中最主要的是動(dòng)態(tài)幾何技術(shù)，可讀證明的產(chǎn)生、組織以及顯示技術(shù)等。本文

2、的主要研究目標(biāo)是為平面幾何研究和設(shè)計(jì)一套能夠高效地輸入、產(chǎn)生以及表示證明的技術(shù)，以幫助用戶更好地理解證明。具體的研究?jī)?nèi)容可以分為以下三個(gè)方面：
　　 1.研究高效率的方法處理幾何圖形中的約束關(guān)系。幾何圖形在幾何定理的證明過(guò)程中起著非常重要的作用。給定一個(gè)幾何定理，畫出其圖形并對(duì)該圖形進(jìn)行變換的過(guò)程可以看做是一個(gè)約束求解的過(guò)程。傳統(tǒng)的約束求解方法沒(méi)有對(duì)約束進(jìn)行統(tǒng)一的處理，因此在求解效率，穩(wěn)定性等方面都存在不小的問(wèn)題。本文研究了如何

3、開(kāi)發(fā)高效的算法對(duì)幾何圖形的約束關(guān)系進(jìn)行求解，希望通過(guò)利用平面幾何定理的一些特殊性質(zhì)，能夠借助強(qiáng)大的代數(shù)方法來(lái)求解幾何圖形中的約束關(guān)系。
　　 2.研究了專門用于幾何定理證明可視化的技術(shù)以及輸入工具。證明文本和幾何圖形的對(duì)應(yīng)關(guān)系是證明可視化技術(shù)的關(guān)鍵。但是對(duì)于傳統(tǒng)的可讀證明來(lái)說(shuō)，這兩者是分開(kāi)的，需要讀者在閱讀的過(guò)程中去比較、識(shí)別它們之間的關(guān)系。對(duì)此，本文研究了平面幾何證明的語(yǔ)法結(jié)構(gòu)，希望能夠給出幾何證明的一般性的結(jié)構(gòu)和組織方式，并

4、且針對(duì)這種格式化的證明提出一種可視化方法，使得我們能夠把證明文本和證明圖形對(duì)應(yīng)起來(lái)。另外，本文研究了可視證明的不同產(chǎn)生方法：一方面，考慮提供手動(dòng)的交互式證明輸入工具，讓用戶使用圖形化的工具建立證明。另一方面，考慮提供自動(dòng)化的方法，充分利用當(dāng)前幾何定理機(jī)器證明領(lǐng)域的研究成果，使得用戶只需要輸入定理文本形式的前提條件就能夠自動(dòng)地產(chǎn)生幾何圖形以及可視證明。
　　 3.研究了動(dòng)態(tài)可視證明的自動(dòng)產(chǎn)生方法以及證明的層次型組織結(jié)構(gòu)。對(duì)于一個(gè)復(fù)

5、雜的幾何定理，當(dāng)它的證明包含了很多步驟時(shí)，如果能夠合理組織證明結(jié)構(gòu)，使得證明能夠保持在合理的長(zhǎng)度之內(nèi)，對(duì)證明的理解顯然非常有幫助。對(duì)此，本文研究了可讀證明的自動(dòng)產(chǎn)生以及組織方法，希望能夠把證明主要的步驟列出來(lái)的同時(shí)，把次要的步驟隱藏起來(lái)，使得用戶在閱讀時(shí)可以抓住證明的重點(diǎn)。
　　 本文對(duì)以上問(wèn)題進(jìn)行了深入研究，并且獲得了一系列研究成果。下面是本文的主要貢獻(xiàn)和創(chuàng)新點(diǎn)：
　　 1.提出了基于構(gòu)造型幾何命題的幾何約束求解方法，

6、利用代數(shù)方程高效地表示和處理幾何圖形的約束關(guān)系。對(duì)于構(gòu)造型幾何命題，根據(jù)幾何命題中點(diǎn)引進(jìn)的順序依次給點(diǎn)的坐標(biāo)參數(shù)賦值，然后把圖形中的約束條件轉(zhuǎn)化成代數(shù)方程組，該方程組可以很容易地三角化。根據(jù)三角化以后的結(jié)果，我們可以高效地對(duì)圖形中的約束進(jìn)行求解。相比較傳統(tǒng)的幾何約束處理方法，該方法具有許多優(yōu)點(diǎn)，例如求解穩(wěn)定，可以計(jì)算出圖形的多種可能情況，并且可以對(duì)幾何圖形的一些隱含的性質(zhì)進(jìn)行推理和證明等。
　　 2.提出了新的基于幾何圖形的證明

7、表示方法-動(dòng)態(tài)可視證明，提出了幾何定理證明的一般語(yǔ)法結(jié)構(gòu)，并且基于這種結(jié)構(gòu)開(kāi)發(fā)了動(dòng)態(tài)可視證明的手動(dòng)輸入方法。動(dòng)態(tài)可視證明最主要的特征是證明的文本和圖形的緊密結(jié)合。在手動(dòng)輸入方法中，證明的語(yǔ)法結(jié)構(gòu)經(jīng)過(guò)了嚴(yán)格的定義，并且根據(jù)這種格式化的證明，采用以鼠標(biāo)操作為主的輸入方式，使得用戶可以在事先知道具體證明的情況下很容易地輸入動(dòng)態(tài)可視證明。
　　 3.提出了基于無(wú)序幾何模型的動(dòng)態(tài)可視證明自動(dòng)產(chǎn)生方法：基于全角法的產(chǎn)生方法和基于演繹數(shù)據(jù)庫(kù)法

8、的產(chǎn)生方法。這兩種方法都是基于無(wú)序幾何的，非常適合算法實(shí)現(xiàn)并且生成動(dòng)態(tài)可視效果。而且，在全角法中，通過(guò)結(jié)合前推法和后推法，我們提出了證明的層次型組織方法。這種方法使得用戶可以把注意力集中在主要的步驟上，而當(dāng)用戶對(duì)某些步驟的進(jìn)一步證明感興趣時(shí)，又可以展開(kāi)這些步驟，查看它們的詳細(xì)證明。在演繹數(shù)據(jù)法中，我們產(chǎn)生一個(gè)包含該幾何定理的許多信息的數(shù)據(jù)庫(kù)，且成功地實(shí)現(xiàn)了數(shù)據(jù)庫(kù)的可視化。
　　 4.基于前面研究成果，我們構(gòu)造了一款幾何定理證明器