1、本學(xué)位論文主要介紹一種用于符號幾何計(jì)算、幾何推理以及視化幾何對象的面向幾何對象語言的設(shè)計(jì)與實(shí)施．這種語言允許用確定的數(shù)據(jù)或不確定的符號來構(gòu)造平面或其它幾何空間中的對象．對構(gòu)造的幾何對象，可以容易地作出如重命名變元、改變參數(shù)值等修改，還可以有效地對它們進(jìn)行基本運(yùn)算和計(jì)算，陳述它們之間的相互關(guān)系并用一種合理的結(jié)構(gòu)來表示這些關(guān)系．通過構(gòu)造的對象以及相互之間的關(guān)系，通常的幾何問題可以用一種特定的規(guī)則來描述，進(jìn)而用高等的方法驗(yàn)證或者證明．根據(jù)這種

2、語言實(shí)現(xiàn)的系統(tǒng)允許用戶進(jìn)行嚴(yán)格精確的幾何計(jì)算和推理、證明和發(fā)現(xiàn)幾何定理、自動生成靜態(tài)或動態(tài)幾何圖形以及交互式的文檔． 在這種語言中，我們采用一種情形區(qū)分技術(shù)來形式化描述符號幾何對象和幾何關(guān)系，該技術(shù)允許遍歷所有可能情形來構(gòu)造和操作幾何對象、進(jìn)行幾何計(jì)算和推理．基于該技術(shù)，本文引入兩個(gè)重要的概念復(fù)合幾何對象和復(fù)合幾何關(guān)系．情形區(qū)分技術(shù)把處理符號幾何對象的不確定性和退化情形轉(zhuǎn)化為處理包含在復(fù)合對象和復(fù)合關(guān)系中邊條件的問題，進(jìn)而推廣到

3、幾何約束處理問題．本文對該問題在約束化簡、檢查相容性、關(guān)系推導(dǎo)等方面進(jìn)行了討論，并給出一些特殊的處理方法． 本文圍繞著這種面向幾何對象語言的設(shè)計(jì)和實(shí)現(xiàn)展開．首先，本文的主體給出有關(guān)幾何計(jì)算和推理方法的綜述，簡單介紹幾何定理機(jī)器證明發(fā)展的情況和一些常用的方法及相關(guān)軟件包．然后，本文詳細(xì)介紹用情形區(qū)分技術(shù)描述幾何對象和關(guān)系的方法，描述這種語言所期望具有的基本功能和整體設(shè)計(jì)思想、所包含的主要組成部分及各部分的基本功能，并給出一個(gè)基于上