基于本體和Prolog規(guī)則的幾何定理證明的研究.pdf

1、隨著計算機技術(shù)的發(fā)展，人工智能技術(shù)取得了突破性的進步。機器定理證明是人工智能領(lǐng)域重要的研究課題，到目前為止已經(jīng)有幾種較為成熟的方法，如吳先生的代數(shù)法、張景中院士的―消點算法、基于規(guī)則的定理證明等，這些方法與傳統(tǒng)的幾何命題證明方法不符。如何能夠以符合人們傳統(tǒng)習(xí)慣的方式來解決幾何定理機器證明問題成為一個重要的研究課題。20世紀末期語義Web本體理論的出現(xiàn)給本文的研究提供了一個方向，本文通過對本體及其相關(guān)理論的研究得到了一種幾何定理證明的方法

2、。該方法用本體模型來對幾何命題知識進行描述，通過基于本體的 Prolog規(guī)則來對幾何定義、定理和公理進行描述，最后通過知識庫推理機來完成幾何定理證明。
　　本研究主要內(nèi)容包括：⑴平面幾何本體模型構(gòu)建方法的研究。通過對本體語言的深入研究，得到一種基于語義的幾何命題描述方法。將幾何命題知識通過本體的類、屬性和個體進行描述。采用本體語言O(shè)WL DL來描述幾何命題的邏輯關(guān)系，原因是該本體語言具有邏輯推理能力，可以實現(xiàn)基于規(guī)則的推理。⑵基于

3、本體與規(guī)則幾何定理證明的研究。首先采用上述方法構(gòu)建平面幾何本體模型。其次，用prolog規(guī)則對幾何定理進行描述。最后將該Prolog規(guī)則作用于平面幾何本體模型完成幾何定理證明。⑶幾何定理規(guī)則半自動生成方法的研究。通過對Prolog規(guī)則和平面幾何本體模型關(guān)系的深入研究，總結(jié)其對應(yīng)關(guān)系，得到了一種可以自動生成幾何定理Prolog規(guī)則約束的方法，該方法可以提高規(guī)則的書寫效率，支持定理可持續(xù)證明。最后，分別設(shè)計了定理規(guī)則半自動生成的實驗和幾何定