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

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

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

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

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

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

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

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

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