《基於本體的幾何定理機器證明》是依託電子科技大學,由符紅光擔任醒目負責人的面上項目。
基本介紹
- 中文名：基於本體的幾何定理機器證明
- 依託單位：電子科技大學
- 項目類別：面上項目
- 項目負責人：符紅光
項目摘要,結題摘要,
項目摘要
定理機器證明是人工智慧研究的重要課題，又屬知識工程的範疇。幾何定理機器證明最早由Hibert提出，50年代初Tarski用代數方法證明了初等幾何機械化的可能性；70年代末，吳文俊院士給出可在計算機上實現的代數特徵列方法；隨後，張景中院士提出具有可讀性的幾何不變數方法。這些方法屬於代數消元法，而邏輯證明一直是人類的夢想，自60年代格蘭特提出後一直進展甚微。最近張景中院士和申請人研究出基於規則的幾何定理證明器，在教育領域取得了很好的套用。但此方法很難明確表達領域知識和實現系統分層。因此，本項目將從更一般的本體知識庫出發，研究在領域層將通用本體和自然語言處理技術用於擴展核心本體，構建幾何知識本體，提供模型化的領域知識；在推理層構建一個集本體、複雜邏輯和符號計算於一體的推理模型，更好地實現知識推理，促進知識的共享和重用，從而為幾何定理機器證明提供一條新途徑，也為類似領域知識的問題求解提供新思路。
結題摘要
本項目從更一般的本體知識庫出發，以“構建領域核心本體→通用本體擴展領域核心本體→自然語言處理技術擴展領域核心本體”的層層遞進的方式，研究在領域層構建一個較完善的幾何知識本體，提供模型化的領域知識；研究推理層的基於本體的推理與規則相結合的混合推理模型，進一步研究計算相關問題的解決方式，建立數值測試推理策略，研究輔助線和輔助點的問題，建立輔助點和輔助線的推理策略，更好地實現知識推理；在此基礎上構建一個集本體、規則推理、符號計算、數值測試、輔助線/點的添加等策略於一體的幾何定理證明器；本項目為幾何定理機器證明提供一條新途徑，也為類似領域知識的問題求解提供新思路。
