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

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

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

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

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