基于網(wǎng)格計算的定理自動證明研究.pdf

1、自動定理證明(又叫機器定理證明、機械化定理證明等)是人工智能研究的一個重要分枝，是數(shù)學(xué)、計算機科學(xué)的交叉學(xué)科，我國科學(xué)家在這一領(lǐng)域的研究走在了世界的前列。不僅提出了多種有效的方法，還成功的開發(fā)了一些智能的定理證明系統(tǒng)，其中一些成果已經(jīng)被成功的應(yīng)用到幾何教育領(lǐng)域。但當(dāng)前機器證明的理論研究進入低潮，自20世紀末以來，國外研究人員嘗試將網(wǎng)絡(luò)并行計算技術(shù)引入到一些關(guān)鍵計算問題中，以求得較高的計算效率，國內(nèi)這方面的研究也處于起步階段。近年來，隨著

2、Web技術(shù)的日益發(fā)展和Internet的廣泛應(yīng)用，越來越多的人開始研究借助網(wǎng)絡(luò)解決數(shù)學(xué)問題，目前絕大部分研究都是以數(shù)學(xué)信息平臺的建設(shè)作為重點，在遠程和分布式的環(huán)境下實現(xiàn)定理的自動證明的研究并不多見。 網(wǎng)格計算是新一代的分布式計算方法，用來表述一種適用于高端科學(xué)和工程的分布式計算的體系結(jié)構(gòu)。與傳統(tǒng)分布式計算的主要區(qū)別在于在沒有集中控制機制的情況下，通過對計算資源進行大規(guī)模共享，滿足應(yīng)用對高性能計算要求，并且這種對計算資源進行大規(guī)模

3、共享是動態(tài)的、柔性的、安全的和協(xié)作式的，解決了常見的網(wǎng)絡(luò)并行計算系統(tǒng)面臨的操作系統(tǒng)、協(xié)議的異構(gòu)性問題。 如果將網(wǎng)格計算的技術(shù)應(yīng)用到幾何定理證明的方法中，就可以利用網(wǎng)格提供的超級計算能力，實現(xiàn)高效的協(xié)作資源共享，提高定理系統(tǒng)的可重用性、交互性及定理證明的效率。本文的工作是以幾何定理證明中的數(shù)值方法為基礎(chǔ)，嘗試將網(wǎng)格計算技術(shù)應(yīng)用于幾何定理自動證明，探究一種基于網(wǎng)格計算的幾何定理證明的實現(xiàn)方法。在充分分析了網(wǎng)絡(luò)并行計算理論和實現(xiàn)技術(shù)的