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

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

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

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

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