基于數(shù)值計算的幾何定理動態(tài)搜索方法的研究與實現(xiàn).pdf

1、定理機器證明是人工智能研究的一個重要課題。在其中的幾何定理機器證明研究領域，我國的科學家最近二十幾年來取得了一系列令世人矚目的成果，提出了吳方法、幾何不變量法、演繹數(shù)據(jù)庫的搜索法，以及數(shù)值并行法等多種不同的方法?；谶@些方法設計開發(fā)的幾何定理證明系統(tǒng)不僅推動了人們對幾何領域問題的研究，也為其它領域的定理自動證明提供了有益的啟示。 目前已有的幾何定理證明方法大多只側(cè)重于幾何定理的嚴格證明，然而人們研究幾何問題時會發(fā)現(xiàn)，除了命題給出

2、的結(jié)論外，一個幾何問題往往還包含很多其它有意義的信息。有時挖掘出人們感興趣的某些幾何關系的有用信息不但有助于命題結(jié)論的證明，而且便于人們更深入透徹的理解一個幾何命題，甚至可以從中發(fā)現(xiàn)新的未知的定理。 已有的方法中，基于演繹數(shù)據(jù)庫的搜索方法雖然可以在證明命題時搜索出其它有用的幾何信息，但是該方法為了證明命題的結(jié)論而采用“大英博物館”式的推理方法，使中間幾何信息過度膨脹，也影響了證明命題的效率。因此，如果能夠找到一個更高效的定理證明

3、方法，可以在證明定理的同時對人為指定的幾何關系進行全面的信息搜索，找出人們關心的幾何關系所有成立的結(jié)論信息，無疑有助于我們更快捷方便的研究和解決幾何問題。 此外，幾何定理自動證明在實現(xiàn)方面還尚有一些需要探索改進的地方，例如進一步提高證明的效率，以及解決非構(gòu)造性命題等。 針對這些問題，本文在數(shù)值方法的基礎上提出了幾何定理的動態(tài)搜索方法，能夠在證明初等平面幾何命題的同時，快速全面的對該命題進行定理信息搜索。該方法采用不同于傳

4、統(tǒng)嚴格的證明方法，而是在搜索的過程中通過隨機舉例的方法證明結(jié)論是否成立，因此效率要比人工智能推理的方法有很大提高。國外這一領域最新的研究結(jié)果表明，概率意義上的驗證方法能夠保證最終結(jié)論正確的概率高達1-ε，因此幾何定理動態(tài)搜索方法能夠快速將絕大部分錯誤信息排除，并且所有正確的信息都包含在最終搜索的信息集合中。 在此基礎上，我們結(jié)合非構(gòu)造性幾何命題的特點對該方法進一步改進，使其同樣能夠解決非構(gòu)造性的初等平面幾何命題。擴展了方法的應用