鐘秀琴，符紅光，丁盤蘋

(電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院 成都 610054)

定理機(jī)器證明(automated theorem proving，ATP)就是把證明定理的一般知識和規(guī)則以適當(dāng)?shù)男问酱鎯Φ接?jì)算機(jī)中，讓計(jì)算機(jī)通過運(yùn)算自動地證明定理，因此也叫自動推理，它既是人工智能研究的重要課題，又屬知識工程的范疇[1]。

幾何定理機(jī)器證明方向在自動推理的研究中占有重要的地位。一方面，我國在該方向上具有領(lǐng)先優(yōu)勢；另一方面，該方向有清晰明確的應(yīng)用背景，近年來在機(jī)器證明領(lǐng)域的研究十分活躍，值得關(guān)注。

到目前為止，幾何定理機(jī)器證明的主要方法有代數(shù)方法、幾何不變量方法和基于演繹數(shù)據(jù)庫(或基于規(guī)則的搜索)等方法。

文獻(xiàn)[2]提出了一個證明等式型初等幾何定理的新的代數(shù)方法，用它可在微型計(jì)算機(jī)上花幾分鐘甚至幾秒鐘證明很不簡單的定理，該方法即吳方法。幾何定理機(jī)器證明的代數(shù)方法以吳方法為代表，吳方法的出現(xiàn)被公認(rèn)為是機(jī)器證明領(lǐng)域里程碑式的突破。后來又出現(xiàn)了如國外的Grobner基方法[3]，國內(nèi)的Dixon消元法、例證法等代數(shù)方法。但它們僅能夠判斷幾何命題的成立與否，且證明過程十分復(fù)雜，需要進(jìn)行大量的數(shù)值計(jì)算和符號計(jì)算，與傳統(tǒng)幾何證明的簡潔明了大相徑庭，人們很難讀懂這些方法生成的證明過程。

文獻(xiàn)[4]以面積法作為基礎(chǔ)，提出消點(diǎn)算法是幾何不變量方法的標(biāo)志性算法。幾何不變量的方法雖然實(shí)現(xiàn)了一大類幾何定理的機(jī)器可讀證明，但是該方法得到的證明過程常常不符合人們的思維習(xí)慣。

基于幾何推理數(shù)據(jù)庫或基于規(guī)則的方法[5]，是根據(jù)幾何命題所給的條件、已知的公理、定理及公式等推理規(guī)則，通過大量的試驗(yàn)匹配的方法進(jìn)行證明。文獻(xiàn)[6]提出了一個基于前推模式的幾何信息搜索系統(tǒng)(GISS)，成功地證明了161個非平凡的幾何命題。但該方法所表現(xiàn)的信息十分豐富，即中間過程的幾何信息呈指數(shù)增長，成為該方法研究的瓶頸。

如何生成讓人容易讀懂的幾何證明過程？該問題成為研究者們面臨的又一個嚴(yán)峻挑戰(zhàn)。本文從理論研究入手，旨在找到一種脫離代數(shù)的幾何定理證明方法，且使其具有接近自然語言的描述，以擺脫只有專家才能讀懂定理機(jī)器證明的尷尬處境。

本體是當(dāng)前的研究熱點(diǎn)，本體可以表示領(lǐng)域內(nèi)概念與概念之間的關(guān)系。到目前為止，本體在很多方面得到了應(yīng)用，如WordNet、Enterprise ontology[7]和Gene ontology[8]等都是典型的本體應(yīng)用。進(jìn)一步，本體可作為信息檢索系統(tǒng)的核心，通過構(gòu)造形式化的領(lǐng)域本體，將知識表示和知識處理引入互聯(lián)網(wǎng)信息處理，為互聯(lián)網(wǎng)上半結(jié)構(gòu)化數(shù)據(jù)和關(guān)系數(shù)據(jù)庫提供統(tǒng)一的語義模型。因此，本文在前人研究與實(shí)踐的基礎(chǔ)上，將本體引入平面幾何定理機(jī)器證明，進(jìn)一步拓展本體模型的應(yīng)用。

本文首先對平面幾何定理證明所需的基礎(chǔ)理論進(jìn)行分析，然后以具體實(shí)例說明領(lǐng)域本體模型的構(gòu)建過程，以及如何將本體推理與規(guī)則推理結(jié)合進(jìn)行幾何定理機(jī)器證明，最后給出整個問題求解的過程和所得到的結(jié)論。

1 平面幾何本體模型的構(gòu)建

1.1 本體相關(guān)概念

本體作為一種能在語義和知識層次上描述信息系統(tǒng)的概念模型的建模工具，被提出后迅速成為信息系統(tǒng)與人工智能領(lǐng)域的研究熱點(diǎn)?！爸R本體(ontology)是共享概念模型的明確的形式化的規(guī)范說明”[9]。該定義包含4層含義。

1) 概念化：通過抽象出客觀世界中一些現(xiàn)象的相關(guān)概念而得到的模型，其含義獨(dú)立于具體的環(huán)境狀態(tài)。

2) 明確：所使用的概念及使用這些概念的約束都有明確(顯式)的定義。

3) 形式化：知識本體是計(jì)算機(jī)可讀的。

4) 共享：知識本體中所體現(xiàn)的是共同認(rèn)可的知識，所反映的是相關(guān)領(lǐng)域中公認(rèn)的概念集，所針對的是團(tuán)體而不是個體。

通過構(gòu)建本體能夠精確規(guī)范某個領(lǐng)域的概念，明確定義機(jī)器可以處理的概念及概念之間的關(guān)系，大大提高知識搜索、知識重用、知識共享的效率。

當(dāng)前，本體構(gòu)建工具主要包括Ontolingua Server、Ontosaurus、WebOnto、OntoEdit、Protégé等[10]，本文研究采用由斯坦福大學(xué)醫(yī)學(xué)信息研究組開發(fā)的Protégé構(gòu)建本體。1) Protégé是一個免費(fèi)和開源的本體編輯平臺，可以使用RDF、RDFS、OWL等本體描述語言編輯和修改本體；2) Protégé可以直接對類、實(shí)例和屬性等進(jìn)行編輯操作，用戶不必掌握具體的本體表示語言；3) 用戶可根據(jù)自己的應(yīng)用需求開發(fā)新插件和定制已有插件；4) Protégé支持中文[10]。

本體描述語言O(shè)WL(web ontology language)是W 3C推薦的語義互聯(lián)網(wǎng)中本體描述語言的標(biāo)準(zhǔn)。按照對本體功能的支持分為OWL Lite、OWL DL和OWL Full。其中OWL DL是基于描述邏輯(description logics)[11]的，它支持那些需要最強(qiáng)表達(dá)能力的推理系統(tǒng)的用戶，且推理系統(tǒng)能夠保證計(jì)算的完全性(computational completeness，即所有的結(jié)論都能夠保證被計(jì)算出來)和可判定性(decidability，即所有的計(jì)算都在有限的時間內(nèi)完成)[12]。因此，本文選擇OWL DL作為本體模型描述語言。

本體模型的構(gòu)建方法很多，有領(lǐng)域?qū)＜沂止?gòu)建的領(lǐng)域本體，有自動或半自動構(gòu)建的本體。本文采用的是基于WordNet重用的領(lǐng)域本體半自動構(gòu)建方法[13]。首先通過WordNet接口提取基本的幾何元素，以及這些元素的上位、下位、兄妹關(guān)系和同義詞等關(guān)系，然后用Protégé編輯領(lǐng)域本體，并根據(jù)幾何定理證明的具體要求，修改或添加一些必要的屬性擴(kuò)充領(lǐng)域本體，存儲為.ow l文件。

1.2 平面幾何本體模型

本體模型主要由如下幾部分組成。

1) 類：一個類是一類個體的集合。一個領(lǐng)域中的最基本概念應(yīng)分別對應(yīng)于各個分類層次樹的根。OWL中的所有個體都是類ow l:Thing的成員，主要包括rdfs:subClassOf、ow l:equivalentClass等關(guān)系。平面幾何定理證明中的基本類包含點(diǎn)類、線類、角類、圓類、多邊形類等?；赪ordNet重用的領(lǐng)域本體半自動構(gòu)建方法構(gòu)建的多邊形的分類關(guān)系如圖1所示，其中長方形和矩形是等價類的關(guān)系。

圖1 類的構(gòu)建示意圖

2) 屬性：屬性是斷言關(guān)于類成員的一般事實(shí)以及關(guān)于個體的具體事實(shí)的依據(jù)，一個屬性是一個二元關(guān)系。基本屬性主要包括ObjectProperty、DatatypeProperty、Domain、TransitiveProperty、SymmetricProperty、FunctionalProperty、InverseOf、Range、HasValue等。此外，在平面幾何定理證明領(lǐng)域，還需要添加一些領(lǐng)域?qū)傩裕糠诸I(lǐng)域?qū)傩匀绫?所示。

表1 領(lǐng)域部分屬性列表

如圖2所示，虛線上方表示構(gòu)建的是具有長度屬性的線段類，屬性類型是數(shù)據(jù)屬性。一個類可具有多個屬性。

3) 個體：類的成員是范疇中的一個個體。類僅是一個名稱和一些描述某集合內(nèi)個體的屬性，而個體是該集合的成員。type表示一個RDF屬性(RDF property)，用于關(guān)聯(lián)一個個體和它所屬的類。

圖2 屬性構(gòu)建示意圖

如圖2所示，虛線下方為屬性構(gòu)建實(shí)例。已知個體“AB”和個體“2”之間具有“長度”屬性，則可推理出“AB是線段”“2是長度值”。相反地，若已知“BC是線段”“2是長度值”，則可推理出“BC”與“2”之間具有“長度”屬性。圖中實(shí)線箭頭表示已知條件，虛線箭頭表示由本體推理出的結(jié)論。

1.3 本體模型構(gòu)建思路

本文采用的是基于WordNet重用的領(lǐng)域本體半自動構(gòu)建方法，并將幾何模型中的基本元素作為本體模型中的類；將基本元素的性質(zhì)及其關(guān)系作為本體模型類的屬性；將幾何定理作為聯(lián)系整個本體模型的規(guī)則；然后將幾何例題作為本體模型的個體進(jìn)行實(shí)例化。

2 基于Prolog規(guī)則的推理

描述邏輯可以執(zhí)行本體推理，但描述邏輯對陳述性知識的表達(dá)能力不足，不能提供關(guān)系間的組合推理。如已知屬性關(guān)系hasFather(Tom,Jack)和關(guān)系hasSpouse(Jack,Rose)，卻無法推理出hasMother(Tom,Rose)，即不能通過描述邏輯的推理。而大多數(shù)的問題求解都涉及復(fù)雜關(guān)系間的組合推理，因此需合理地將規(guī)則推理與本體推理相結(jié)合。

規(guī)則可遵循多種語法，常用的有SPARQL、Prolog等，本文使用Prolog進(jìn)行規(guī)則描述。如線段相等，可用規(guī)則描述如下：

可以通過查詢語句(select(?x ?y)(線段相等?x ?y))得到實(shí)例模型中所有相等的線段，由此可以判斷線段AB和線段BC相等。該方法可應(yīng)用于平面幾何定理證明。

3 平面幾何案例設(shè)計(jì)及實(shí)現(xiàn)

例：已知任意四邊形ABCD，點(diǎn)E、F、G、H分別是線段AB、BC、CD、DA的中點(diǎn)，如圖3所示。證明四邊形EFGH是平行四邊形。

考慮到目前的推理系統(tǒng)有前推系統(tǒng)(根據(jù)已知事實(shí)及相關(guān)的性質(zhì)定理進(jìn)行前向推理)、后推系統(tǒng)(從目標(biāo)及相關(guān)的定義、判定定理進(jìn)行后向推理)和將二者結(jié)合的雙向推理系統(tǒng)。本文中采用的是雙向推理的方法。

圖3 實(shí)例示意圖

表2 已知對象類的相關(guān)性質(zhì)定理

1) 前推法分析。分析本例的已知條件，有點(diǎn)類、線段類、三角形類、四邊形類、中點(diǎn)類等，每個類有與其相關(guān)的性質(zhì)、定理及與其對應(yīng)的本體模型。表2所示為已知對象類的相關(guān)性質(zhì)、定理，表中列出了相應(yīng)定理的結(jié)論。

三角形類的部分本體模型如圖4所示，該圖描述了與本例相關(guān)的三角形的屬性、線段的屬性、點(diǎn)的屬性及部分實(shí)例等。三角形有邊、有頂點(diǎn)的屬性是從多邊形繼承來的，即由rdfs:subClassOf推理得出的。

進(jìn)一步，由對表2的分析可以看出，與平行關(guān)系和線段等量關(guān)系相關(guān)的定理只有三角形中位線定理，而三角形中位線的本體模型描述如圖5的虛線上方部分所示，虛線下方部分為三角形的中位線所具有性質(zhì)的定理，可描述三角形的中位線所具有的屬性。三角形的中位線的Prolog規(guī)則描述如下：

圖4 三角形部分本體模型圖

根據(jù)上述Prolog規(guī)則，可由建立的本體模型推理出f表示三角形，d表示三角形的中位線，z表示三角形的底邊。通過三角形的中位線性質(zhì)的定理可得出三角形的中位線與三角形的底邊的關(guān)系為“三角形的中位線平行于第3邊(底邊)，且等于第3邊(底邊)的一半”，因此可建立三角形的中位線的平行關(guān)系屬性和線段等量關(guān)系屬性(等于1/2)，且兩個屬性都具有傳遞性(transitivity)。因此，根據(jù)上述Prolog規(guī)則和傳遞性的約束屬性，可由前推法得到相關(guān)結(jié)論，如表3所示。

圖5 三角形的中位線模型及其性質(zhì)定理

表3 本體和規(guī)則推理結(jié)果

2) 后推法分析。分析本例中的結(jié)論為“四邊形是平行四邊形”，需用到相關(guān)的判定定理如表4所示。基于本體的平行四邊形后推法模型可描述為如圖6所示的過程。

表4 “四邊形是平行四邊形”結(jié)論的判定定理

四邊形類的本體描述從略，其屬性還包括對邊、鄰邊等。如圖6所示，要證明四邊形為平行四邊形，可通過平行四邊形的定義和平行四邊形的判定定理1～4等進(jìn)行證明。定義平行四邊形，需定義其兩組對邊分別平行。因此其相應(yīng)的Prolog規(guī)則描述如下：

由表3、表4和該平行四邊形的Prolog規(guī)則，即可推理出該四邊形EFGH為平行四邊形，從而基于本體和Prolog規(guī)則的推理描述結(jié)束。

圖6 基于本體的后推法

最后，將本體實(shí)例模型保存為.ow l文件。支持ow l的推理機(jī)很多，如RACER、FaCT、Pellet、Jena等。本文采用基于Jena和Prolog的A llegro Graph(AG)數(shù)據(jù)庫進(jìn)行推理，因?yàn)锳G數(shù)據(jù)庫提供了外部調(diào)用的API，而且AG數(shù)據(jù)庫存取數(shù)據(jù)的方式是三元組形式，與上述的模型描述一致，存取的形式接近自然語言。將上述本體實(shí)例模型和Prolog規(guī)則導(dǎo)入AG數(shù)據(jù)庫，則得到平行四邊形EFGH。至此，本文例題的平面幾何定理證明圓滿完成。

4 結(jié) 論

本文通過對本體理論、本體建模、基于Prolog的推理等方面的研究和對例題證明過程的設(shè)計(jì)與實(shí)現(xiàn)，驗(yàn)證了基于本體和Prolog規(guī)則進(jìn)行平面幾何定理證明的可行性。雖然尚不能確定這是一種快速的方法，但是完全有理由相信這是一種有前途的機(jī)器證明方法。

首先，基于本體的方法很好地體現(xiàn)了概念及其關(guān)系之間的層次性和結(jié)構(gòu)性，以及關(guān)系之間的約束性，基于Prolog規(guī)則的方法很好地解決了復(fù)雜的關(guān)系間的組合推理。將兩種方式結(jié)合，可有效地規(guī)避問題求解中的多次判斷問題。其次，可將問題分析和推理同步進(jìn)行，證明的效率可得到較大的提高。再次，基于本體和Prolog規(guī)則的幾何定理證明是接近自然語言的證明方法，是定理機(jī)器證明的新思路，且本體模型的構(gòu)建及其推理還可進(jìn)一步應(yīng)用于數(shù)據(jù)挖掘，為行業(yè)用戶提供精確的信息檢索、智能推送等服務(wù)。

[1] 趙子都. 定理機(jī)器證明[J]. 自然辯證法研究, 1994, 10(5):46-50.

ZHAO Zi-du. The machine demonstration of theorems[J].Studies in Dialectics of Nature, 1994, 10(5): 46-50.

[2] 吳文俊. 初等幾何判定問題與機(jī)械化證明[J]. 中國科學(xué)(A輯), 1977, 20(6): 507-516.

WU Wen-jun. on the decision problem and the mechanization of theorem in elementary geometry[J].Science in China, Ser A, 1977, 20(6): 507-516.

[3] BOSE N K. Multidimensional systems theory[M]. [S.l.].Reidel Publishing Company, 1985: 184-232.

[4] ZHANG Jin-zhong, ZHOU Xian-qing, GAO Xiao-shan.Automated production of traditional proofs for theorems in euclidean geometry[J]. Annals of Mathematics and Arti fi cial Intelligence, 1995, 13: 109.

[5] FU Hong-guang, ZHONG Xiu-qin, ZENG Zhen-bing.Automated and readable simplification of trigonometric expressions[J]. Mathematical and Computer Modeling, 2006,44(11-12): 1169-1177.

[6] ZHOU Xian-qing, Gao Xiao-shan, Zhang Jin-zhong. A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Automated Reasoning, 2000, 25(3):219-246.

[7] REN Nan, LIU Jian-yi, GE Shi-lun. Enterpise ontology for supporting M IS design[C]//Proceedings of the Seventh International Conference on Information and Management Sciences. Urumchi, China: China Academic Journal Electronic Publishing House, 2008: 77-80.

[8] LI Li-sha, ZHANG Ning-bo, LI Shao. Ranking effects of candidate drugs on biological process by integrating network analysis and Gene ontology[J]. Chinese Science Bulletin, 2010, 55(26): 2974-2980.

[9] 王長霞, 李冠宇, 陳布偉. 語義網(wǎng)本體構(gòu)建工具現(xiàn)狀及發(fā)展趨勢研究[J]. 計(jì)算機(jī)與現(xiàn)代化, 2009, 缺卷號(7): 26-31.

WANG Chang-xia, LI Guan-yu, CHEN Bu-wei, Study on present situation and development trend of ontology construction tools[J]. Computer and Odernization, 2009, 缺卷號(7): 26-31.

[10] STUDER R, BENJAM INS V R, FENSEL D. Know ledge engineering, principles and methods[J]. Data & Know ledge Engineering, 1998, 25(1): 161-197.

[11] BAADER F, CALVANESE D, DEBORAH L. et al. The description logic handbook: Theory, imple mentation and application[M]. Cambridge: Cambridge University Press,2002.

[12] M ICHAEL K S. OWL Web Ontology Language Guide[DB/OL]. [2011-01-12]. http://www.w3.org/TR/2004/ REC-ow l-guide-20040210.

[13] 趙天忠, 苗壯, 張亞飛. 基于WordNet重用的領(lǐng)域本體構(gòu)建方法[J]. 系統(tǒng)仿真學(xué)報(bào), 2007, 19(19): 4583-4586.

ZHAO Tian-zhong, M IAO Zhuang, ZHUANG Ya-fei.Reusing WordNet for building domain ontology[J]. Journal of System Simulation, 2007, 19(19): 4583-4586.

編 輯 蔣 曉