一種基于圖的DL-Lite本體最小不可滿足保持子集的計(jì)算方法

付雪峰,漆桂林,張 勇

(1.南昌工程學(xué)院信息工程學(xué)院，江西南昌 330099；2.東南大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院,江蘇南京210096)

?

一種基于圖的DL-Lite本體最小不可滿足保持子集的計(jì)算方法

付雪峰1,漆桂林2,張 勇2

(1.南昌工程學(xué)院信息工程學(xué)院，江西南昌 330099；2.東南大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院,江蘇南京210096)

演變中的本體常出現(xiàn)不一致性問題,這將導(dǎo)致標(biāo)準(zhǔn)推理失效.針對(duì)不一致性問題,最小不可滿足保持子集能夠提供本體中概念不可滿足的解釋.計(jì)算最小不可滿足保持子集是本體工程中的一項(xiàng)重要的非標(biāo)準(zhǔn)推理任務(wù),但多數(shù)計(jì)算方法須借助外部的推理機(jī),導(dǎo)致計(jì)算的效率不高.為了減少對(duì)推理機(jī)的依賴,本文提出了一種基于圖的最小不可滿足保持子集的計(jì)算方法.新的方法面向DL-Lite描述邏輯家族,將DL-Lite本體轉(zhuǎn)換成圖,將本體中的最小不可滿足保持子集轉(zhuǎn)換成圖上的最小不可滿足保持路徑對(duì).對(duì)比實(shí)驗(yàn)表明,基于圖的方法提高了計(jì)算的效率和穩(wěn)定性.

本體;描述邏輯;不一致處理;最小不可滿足保持子集

1 引言

在實(shí)際應(yīng)用中,基于描述邏輯的本體常處于擴(kuò)展、重用、融合等演變過程中,這可能導(dǎo)致本體中出現(xiàn)不一致[1],也因此使得本體推理的失敗[2].本體調(diào)試是一種常用的處理不一致問題的方法,它旨在尋求本體中導(dǎo)致沖突的最小不一致子集[3].對(duì)于導(dǎo)致不一致的原因,Schlobach等認(rèn)為是由于本體中存在不可滿足概念或角色,他們提出了最小不可滿足保持子集(Minimal Unsatisfiability-Preserving Subset,MUPS)的概念來解釋概念或角色不可滿足的原因[4].對(duì)于MUPS的計(jì)算,Kalyanpur等提出基于碰集樹的計(jì)算方法[5],但碰集樹算法復(fù)雜度太高.為了提高計(jì)算效率,Suntisrivaraporn等通過模塊抽取的方法來優(yōu)化MUPS的計(jì)算[6],但該方法抽取的模塊過大導(dǎo)致計(jì)算效率提升不明顯且需要反復(fù)調(diào)用外部推理機(jī).為減少對(duì)推理機(jī)的依賴,本文尋求借助于圖的方法來完成MUPS的計(jì)算.基于圖的方法常用于查詢應(yīng)答,如Qin等提出了一種基于圖的查詢重寫方法[7].在分類任務(wù)方面,Lembo等提出了基于圖的本體分類的方法[8],但該方法僅涉及肯定包含公理.在不一致處理方面,Qi等提出了一種基于圖的ABox修正方法[9],但它沒有考慮TBox中的不一致性問題.為此,本文提出了一種基于圖的MUPS計(jì)算方法.在方法中DL-Lite本體被轉(zhuǎn)換成有向圖,在圖上定義了與MUPS相對(duì)應(yīng)的概念MUPP(最小不可滿足保持路徑),并證明了兩者在表達(dá)能力上是等價(jià)的.最后,基于圖數(shù)據(jù)庫實(shí)現(xiàn)了本文的計(jì)算方法,對(duì)比實(shí)驗(yàn)表明基于圖的計(jì)算方法在運(yùn)行效率和穩(wěn)定性上要明顯優(yōu)于其他基于推理機(jī)的計(jì)算方法.

2 理論基礎(chǔ)

本文的研究對(duì)象是描述邏輯中的DL-Lite家族,它們能保證推理在多項(xiàng)式時(shí)間內(nèi)完成,同時(shí)又能夠捕獲實(shí)體關(guān)系模型以及統(tǒng)一建模語言中類的大部分知識(shí)[10].DL-Lite的概念和角色的形式化定義如下[10]:

B::=A|?RR::=P|P-C::=B|BE::=R|R

其中,A表示原子概念,P表示原子角色,P—是原子角色的逆,B表示基本概念,其語法形式為原子概念或者為?R;R表示基本角色,其語法形式為原子角色或者原子角色的逆;C表示一般概念,其語法形式為基本概念或者基本概念的否定;E表示一般角色,其語法形式為基本角色或者基本角色的否定.

一個(gè)DL-Lite本體由術(shù)語斷言集合與實(shí)例斷言集合組成,記為O=〈T,A〉.T是術(shù)語斷言集合,其語法形式為BC.A是實(shí)例斷言集合,包括概念實(shí)例斷言和角色實(shí)例斷言.在DL-Lite的子語言中,DL-LiteR擴(kuò)充了角色包含公理,其語法形式為RE;DL-LiteF擴(kuò)充了函數(shù)斷言,其語法形式為(functR).在本體中,形如B1B2或R1R2的公理我們稱為肯定包含公理,形如B1B2或R1R2的公理我們稱為否定包含公理.Calvanese等在文獻(xiàn)[10]中定義了否定包含公理的演繹閉包c(diǎn)ln(T)和肯定包含公理的演繹閉包c(diǎn)lp(T),記cl(T)=clp(T)∪cln(T).描述邏輯通過解釋來描述語義,一個(gè)解釋I=〈ΔI,·I〉,其中ΔI為非空的解釋域,·I為解釋域上的解釋函數(shù).解釋函數(shù)將概念A(yù)解釋為集合AI(AIΔI),將原子角色P解釋為關(guān)系PI(PIΔI×ΔI).對(duì)于一個(gè)DL-Lite公理φ和一個(gè)解釋I,如果滿足Iφ,則I為公理φ的一個(gè)模型;如果解釋I滿足本體O中任意的公理,則I為本體O的一個(gè)模型,如果本體O的所有模型也是公理φ的模型,則稱本體O蘊(yùn)含φ,記為Oφ.接下來將引入一些概念來描述本體中的不一致問題.

定義1 不可滿足概念或者角色[4].如果一個(gè)概念C(或角色R),對(duì)于TBoxT的任意一個(gè)模型I,都有CI=?(或者RI=?),那么概念C(或角色R)就被稱為T的一個(gè)不可滿足概念(或角色).

對(duì)一個(gè)不可滿足概念或角色而言,其MUPS并不是唯一的,我們將TBoxT中關(guān)于C的所有MUPS記為mups(C,T).如果本體中存在不可滿足概念或角色,則該本體是不協(xié)調(diào)的,在本體不協(xié)調(diào)的問題中,最小不可滿足保持子集與不可滿足概念密切相關(guān).

定義2 最小不可滿足保持子集[4].設(shè)C(R)是TBoxT中的任意一個(gè)不可滿足概念(或者角色),一個(gè)TBoxT′T是T中關(guān)于概念C(或者角色R)的最小不可滿足保持子集(MUPS)當(dāng)且僅當(dāng)C(或者角色R)在T′中是不可滿足的,且對(duì)于T′的任何一個(gè)真子集T″?T′,概念C(或者角色R)在T″上是可滿足的.

3 本體到圖的轉(zhuǎn)換

為了實(shí)現(xiàn)基于圖的MUPS計(jì)算,需要將TBox轉(zhuǎn)換成有向圖.給定一個(gè)DL-Lite的TBoxT以及T上的符號(hào)集合ΣT;一個(gè)與TBox對(duì)應(yīng)的有向圖,記為GT=〈V,E〉(V是圖上頂點(diǎn)的集合,E是圖上邊的集合),可以通過如下的規(guī)則構(gòu)造[11]:

(1)對(duì)于ΣT中的任意的概念A(yù),V中包含節(jié)點(diǎn)A.

(2)對(duì)于ΣT中的任意的角色P,V中包含節(jié)點(diǎn)P,P-,?P,?P-.

(3)如果在T中存在公理BC,則在有向圖GT中有邊〈B→C〉∈E并且節(jié)點(diǎn)B,C∈V.

(4)如果在T中存在公理BC,則在有向圖GT中有邊〈B→C〉∈E并且節(jié)點(diǎn)B,C∈V.

(5)如果在T中存在公理R1R2,則在有向圖GT中有邊〈R1→R2〉∈E,〈?R1→?R2〉∈E,〈??,并且節(jié)點(diǎn)R1,R2,?R1,?R2,?,?V.

例1給定一個(gè)DL-Lite的TBoxT={AB,BC,CD,BC,R1R2,B?R1,?R2D},其中A、B、C、D為概念,R1和R2為角色.根據(jù)圖的構(gòu)造規(guī)則,我們得到T對(duì)應(yīng)的有向圖,如圖1所示.

在本體到圖的轉(zhuǎn)換中,由于TBox中可能存在等價(jià)關(guān)系或相互包含的概念或角色,這樣在轉(zhuǎn)換后的有向圖中將存在環(huán)路,即在有向圖中存在強(qiáng)連通分支.而強(qiáng)連通分支的存在將增加路徑計(jì)算的復(fù)雜性,因而有必要對(duì)有向圖中的強(qiáng)連通分支做進(jìn)一步的處理,圖2所示為處理強(qiáng)連圖分支的一個(gè)示例.

圖2的左側(cè)部分為原始的有向圖,虛線框中為強(qiáng)連通分支,強(qiáng)連通分支的獲取可以應(yīng)用Kosaraju-Sharir算法[12]來完成.在獲取了強(qiáng)連通分支后,使用一個(gè)節(jié)點(diǎn)來代替該強(qiáng)連通分支就能實(shí)現(xiàn)對(duì)有向圖中環(huán)的消除,如圖2右側(cè)所示.

接下來我們將討論本體中的包含公理與圖上節(jié)點(diǎn)的連通性之間的關(guān)系.對(duì)于TBoxT={A1A2,A2A3},根據(jù)推理規(guī)則,TA1A3.應(yīng)用圖的構(gòu)造規(guī)則,T轉(zhuǎn)換后的圖GT中存在節(jié)點(diǎn)A1、A2、A3和有向邊〈A1→A2〉、〈A2→A3〉,根據(jù)圖的傳遞閉包,節(jié)點(diǎn)A1可達(dá)節(jié)點(diǎn)A3.從中可看出本體中包含公理的蘊(yùn)含與有向圖上節(jié)點(diǎn)間的可達(dá)性存在對(duì)應(yīng)關(guān)系.為了描述這種關(guān)系,我們將文獻(xiàn)[8]中關(guān)于本體蘊(yùn)含的定理以及包含公理與圖上可達(dá)性的對(duì)應(yīng)關(guān)系的定理擴(kuò)展到否定包含公理[11].

定理1 給定一個(gè)DL-Lite TBoxT,若S1、S2為原子概念或者原子角色,則TS1S2當(dāng)且僅當(dāng)下面至少一個(gè)條件成立:

(1)存在肯定包含公理集合PT(P可以為空)和一個(gè)否定包含公理φ∈T,使得P∪{φ}S1S2;

(2)TS1S1.

4 基于圖的MUPS計(jì)算方法

為了實(shí)現(xiàn)圖上完成MUPS的計(jì)算,我們?cè)趫D上對(duì)MUPS做相應(yīng)的描述.

定義3 最小的不可滿足保持路徑對(duì).假設(shè)T是一個(gè)DL-Lite TBox,T對(duì)應(yīng)的有向圖記為GT=〈V,E〉.對(duì)于V中的任意結(jié)點(diǎn)C,如果在GT中存在一條從結(jié)點(diǎn)C到結(jié)點(diǎn)D的路徑(無環(huán))和一條從結(jié)點(diǎn)C到結(jié)點(diǎn)D的路徑(無環(huán)),則稱這兩條路徑為關(guān)于結(jié)點(diǎn)C的最小的不可滿足保持路徑對(duì)(Minimal Unsatisfiability-Preserving Path-Pair,MUPP),圖GT中關(guān)于結(jié)點(diǎn)C的MUPP的集合記為mupp(C,GT).

圖上的MUPP與本體中的不可滿足概念之間存在對(duì)應(yīng)的關(guān)系.

定理3 假設(shè)T是一個(gè)DL-Lite TBox,GT=〈V,E〉是T對(duì)應(yīng)的有向圖.若C(或R)為T中的概念(或角色),則C(或R)是不可滿足的當(dāng)且僅當(dāng)GT中至少存在一個(gè)關(guān)于結(jié)點(diǎn)C(或R)的MUPP.

證明 (?)若GT中存在一個(gè)關(guān)于結(jié)點(diǎn)C的MUPP,不妨假定該MUPP中的路徑對(duì)為{path{C,D},path{C,D}},這樣在中必定存在〈C→D〉∈E*和〈C→D〉∈E*.根據(jù)定理2,若中包含〈C→D〉和〈C→D〉,則CD∈cl(T)且CD∈cl(T),因而TCC,即C是一個(gè)不可滿足概念.

(?)如果C是一個(gè)不可滿足的概念,則存在一對(duì)不相交概念,(不失一般性,用D和D表示這兩個(gè)概念),T中存在兩個(gè)公理集合滿足TCD且TCD[13],即公理CD和CD都屬于cl(T).根據(jù)定理2可得,中必定包含有向邊〈C→D〉和〈C→D〉,因此在有向圖GT中存在兩條路徑{path{C,D},path{C,D}},即存在關(guān)于C的一個(gè)MUPP.對(duì)于角色R可類似證明.

根據(jù)圖的構(gòu)建規(guī)則,圖GT中的有向邊都對(duì)應(yīng)到包含公理,因而GT中的路徑P對(duì)應(yīng)到T中的公理的集合,不妨將此公理集合記為TP,顯然TPcl(T).如果T存在一個(gè)子集S滿足STp,并且對(duì)于任一S的真子集S′?S,S′TP.我們稱S為T中對(duì)應(yīng)有向圖中的路徑P的最小公理集合.

定理4 假設(shè)T是一個(gè)DL-Lite TBox,GT=〈V,E〉為T對(duì)應(yīng)的有向圖.若GT中存在關(guān)于結(jié)點(diǎn)C的MUPP,我們TBox中與該MUPP相對(duì)應(yīng)的最小公理集合記為ST→C-MUPP,則ST→C-MUPP是T中關(guān)于概念C的一個(gè)MUPS,且mupp(C,GT)中所有關(guān)于結(jié)點(diǎn)C的MUPP所對(duì)應(yīng)的最小公理集合ST→C-MUPP為mups(C,T).

對(duì)于mupp(C,GT)中任意一個(gè)節(jié)點(diǎn)C的MUPP,ST→C-MUPP是T中對(duì)應(yīng)到MUPP的最小公理集合.由于ST→C-MUPP是T中關(guān)于概念C的一個(gè)MUPS,因此ST→C-MUPP∈mups(C,T).對(duì)于mups(C,T)中任意一個(gè)關(guān)于概念C的MUPS,假定該MUPS對(duì)應(yīng)的公理集合為M.根據(jù)定義1,MCC,且M的任意一個(gè)真子集M′?M,M′CC.因此,根據(jù)圖的構(gòu)建規(guī)則M對(duì)應(yīng)的圖GM中存在關(guān)于結(jié)點(diǎn)C的MUPP,而GM′中不存在關(guān)于結(jié)點(diǎn)C的MUPP,即M為T中對(duì)應(yīng)到圖上節(jié)點(diǎn)C的MUPP的最小集合,M包含于集合ST→C-MUPP.

定理4建立了圖上的MUPP與本體中的MUPS之間的聯(lián)系,在此基礎(chǔ)上,我們給出基于圖的MUPS計(jì)算方法CalMUPSonGraph,如算法1所示.

算法1 CalMUPSonGraph

輸入:不協(xié)調(diào)的TBoxT

輸出:所有的mups(C,T)

1. constructGT= 〈V,E〉;

2. mupp:=?;mups:=?;

5. for eachn∈unsat Setdo{

6. mupp:=mupp∪{path(n,S),path(n,S);}}

7. for each mu in mupp do{

8. axiomset:=?;

9. for each pathpi∈mu do{

10. for each edge 〈n1→n2〉∈pido {

11. ifn1=?R1andn2=?R2and 〈R1→R2〉∈GTthen

12. axiomset:=axiomset∪{R1R2};

13. else

14. axiomset:=axiomset∪{n1n2};}}

15. mups:=mups∪axiomset;}

16. return mups;

例2 考慮例1中的TBoxT,應(yīng)用算法CalMUPSonGraph計(jì)算T中所有的MUPS.

CalMUPSonGraph首先將T構(gòu)造成如圖1所示有向圖;在圖中有兩對(duì)不相交的節(jié)點(diǎn){C,C}和{D,D};接下來計(jì)算不相交節(jié)點(diǎn)對(duì)的公共子類,可得節(jié)點(diǎn)對(duì){C,C}的公共子節(jié)點(diǎn)是{A,B}、節(jié)點(diǎn)對(duì){D,D}的公共子節(jié)點(diǎn)是{A,B},節(jié)點(diǎn)A、B即對(duì)應(yīng)不可滿足概念(角

色);之后,計(jì)算節(jié)點(diǎn)A、B到不相交節(jié)點(diǎn){C,C}的路徑對(duì)以及節(jié)點(diǎn)A、B到不相交節(jié)點(diǎn){D,D}的路徑對(duì),根據(jù)定義3,這些路徑對(duì)就是MUPP.例2中的MUPP結(jié)果如圖3所示,圖的左邊為mupp(B,GT),右邊為mupp(A,GT).將MUPP轉(zhuǎn)換成MUPS,將得到:mups(B,T)={{BC,BC}{BC,CD,B?R1,R1R2,?R2D}},mups(A,T)={{AB,BC,BC},{AB,BC,CD,B?R1,R1R2,?R2D}}.

基于圖的MUPS的計(jì)算方法的主要過程是對(duì)圖的遍歷,圖上計(jì)算一個(gè)MUPP能在多項(xiàng)式時(shí)間內(nèi)完成,但在最壞的情況下可能存在指數(shù)多個(gè)MUPS[14],因而對(duì)應(yīng)于圖上也可能存在指數(shù)多個(gè)MUPP,這導(dǎo)致算法達(dá)到指數(shù)級(jí)別的復(fù)雜度.

5 實(shí)驗(yàn)評(píng)估

本節(jié)將本文的方法與其他基于主流推理機(jī)的計(jì)算方法作性能上的對(duì)比,實(shí)驗(yàn)中的本體來源不同的學(xué)科,這些本體并不完全遵循DL-Lite的語法規(guī)范,為此我們對(duì)其做特定的轉(zhuǎn)換處理,如對(duì)形如A∪BC的公理,轉(zhuǎn)換為AC和BC.另外,源本體大多是協(xié)調(diào)的,預(yù)處理中將向本體注入導(dǎo)致某些概念或者角色不滿足的公理,如對(duì)形如{AB,BC,BD}的TBox,向其添加公理{CD}使概念A(yù)、B不可滿足.上述處理可以參用文獻(xiàn)[15]中提供的不一致注入工具(http://jfdu.limewebs.com/dbo-debug/tools.html#injector).實(shí)驗(yàn)軟硬件環(huán)境如下:處理器為Intel Core i5主頻為3.1GHz,JAVA堆的大小為6GB;各推理機(jī)為:Pellet 2.3.1,Hermit1.3.8,FaCT++1.6.3,JFaCT1.2.1.

實(shí)驗(yàn)中本體到圖的轉(zhuǎn)換需要耗費(fèi)一定的計(jì)算時(shí)間,但就MUPS的計(jì)算任務(wù)而言,圖轉(zhuǎn)換的過程能夠以離線的方式完成并且只需運(yùn)行一次,為了更詳細(xì)記錄實(shí)驗(yàn),我們列出本體到圖的轉(zhuǎn)換時(shí)間,如表1所示:

表1 本體到圖的轉(zhuǎn)換時(shí)間(單位:ms)

文中的實(shí)驗(yàn)采用兩種模式,一種模式在各類本體上展開計(jì)算實(shí)驗(yàn),記錄時(shí)間來比較各方法的執(zhí)行效率;另一模式是通過向同一個(gè)本體中不斷增加不可滿足概念或者角色的數(shù)量,比較在沖突信息增量的情況下各個(gè)方法計(jì)算時(shí)間的變化.

表2中記錄的是第一種模式下各個(gè)方法的實(shí)驗(yàn)結(jié)果(CalMUPSonGraph 縮寫為onGraph).

表2 各方法計(jì)算MUPS所耗費(fèi)時(shí)間(單位:ms)

從表2提供的實(shí)驗(yàn)結(jié)果來看,基于圖的MUPS計(jì)算方法的效率要好于其他方法,特別是在大規(guī)模的本體上,如GO和FMA,算法的執(zhí)行時(shí)間有顯著的差異;在小本體上,各方法的計(jì)算速度都比較快,性能差異并不明顯.總體說來,本體規(guī)模越小以及MUPS的數(shù)量越少,計(jì)算MUPS所耗費(fèi)的時(shí)間就越少.

沖突信息增量模式下的實(shí)驗(yàn)結(jié)果如表3所示.由于GO本體規(guī)模較大且在前一個(gè)實(shí)驗(yàn)中各方法在GO上的運(yùn)行時(shí)間差異比較明顯,便于效率的對(duì)比,因此增量實(shí)驗(yàn)選擇GO本體做載體.

表3 增量實(shí)驗(yàn)中計(jì)算MUPS所耗費(fèi)時(shí)間(單位:ms)

從表3同樣可以發(fā)現(xiàn),基于圖的計(jì)算方法的執(zhí)行效率上要優(yōu)于各對(duì)比方法.由于基于JFaCT的方法出現(xiàn)內(nèi)存溢出的情況,在后續(xù)的討論中將剔除該方法.為了便于觀察,我們將增量實(shí)驗(yàn)的結(jié)果表示成圖4所示.

從圖中可以看出,隨本體中不可滿足概念和角色的增加,所有方法的執(zhí)行時(shí)間都隨之增加.其中,基于Pellet和FaCT++的計(jì)算方法耗費(fèi)的時(shí)間很接近,增量的曲線也很相似;基于Hermit的計(jì)算方法耗費(fèi)的時(shí)間最多并且增量曲線最陡,這表明該方法最不穩(wěn)定.基于圖的方法耗費(fèi)的時(shí)間最少,并且執(zhí)行時(shí)間的增量曲線最為平穩(wěn),表明該方法在沖突信息增量的情況下,計(jì)算時(shí)間的增量比較均勻,算法的穩(wěn)定性較好.

6 結(jié)束語

本文提出了一種基于圖的MUPS計(jì)算方法,該方法依據(jù)構(gòu)建規(guī)則將本體轉(zhuǎn)換成有向圖并在圖上定義最小不可滿足保持路徑對(duì).實(shí)驗(yàn)結(jié)果表明,新方法有效的提高了MUPS計(jì)算的效率.下一步我們考慮將該方法推廣到表達(dá)力更強(qiáng)的描述邏輯語言以及考慮應(yīng)用并行的技術(shù)擴(kuò)展基于圖的MUPS計(jì)算方法.

[1]Console M,Lenzerini M.Data quality in ontology-based data access:the case of consistency[A].Proceedings of the 28th AAAI Conference on Artificial Intelligence[C].Québec:AAAI Press,2014.1020-1026.

[2]Carnielli W A,Marcos J.Ex contradictione non sequitur quodlibet[J].Bulletin of Advanced Reasoning and Knowledge,2001,27(1):89-109.

[3]de la Banda M J,Stuckey P J,Wazny J.Finding all minimal unsatisfiable subsets[A].Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming[C].Uppsala:ACM,2003.32-43.

[4]Schlobach S,Cornet R.Non-standard reasoning services for the debugging of description logic terminologies[A].Proceedings of the 18th International Joint Conf.on Artificial Intelligence[C].San Francisco:Morgan Kaufmann Publishers,2003.355-362.

[5]Kalyanpur A,Parsia B,Horridge M,et al.Finding all justifications of OWL DL entailments[A].Proceedings of the 6th International Semantic Web Conference[C].Berlin:Springer,2007.267-280.

[6]Suntisrivaraporn B,Qi G,Ji Q,et al.A modularization-based approach to finding all justifications for OWL DL entailments[A].Proceedings of the 3rd Asian Semantic Web Conference[C].Berlin:Springer,2008.1-15.

[7]Qin B,Wang S,Du X,et al.Graph-based query rewriting for knowledge sharing between peer ontologies[J].Information Science,2008,178(18):3525-3542.

[8]Lembo D,Santarelli V,Savo D F.Graph-based ontology classification in OWL 2 QL[A].Proceedings of the 26th International Workshop on Description Logics[C].Ulm:CEUR-WS,2013.747-759.

[9]Qi G,Wang Z,Wang K,et al.Approximating model-based ABox revision in DL-Lite:theory and practice[A].Proceedings of the 29th AAAI Conference on Artificial Intelligence[C].Menlo Park:AAAI Press,2015.254-260.

[10]Calvanese D,De Giacomo G,Lembo D,et al.Tractable reasoning and efficient query answering in description logics:the DL-Lite family[J].Journal of Automated Reasoning,2007,39(3):385-429.

[11]Fu X,Zhang Y,Qi G.A graph-based approach to antology debugging in DL-Lite[A].Proceedings of the 4th Joint International Conference on Semantic Technology[C].Berlin:Springer,2014.33-46.

[12]Sharir M.A strong-connectivity algorithm and its applications in data flow analysis[J].Computers and Mathematics with Applications,1981,7(1):67-72.

[13]周麗平,黃厚寬,漆桂林,等.一種在DL-Lite中計(jì)算本體最小不可滿足保持子集的算法[J].計(jì)算機(jī)研究與發(fā)展,2011,48(12):2334-2342.

Zhou Li-ping,Huang Hou-kuang,Qi Gui-lin,et al.An algorithm for calculating minimal unsatisfiability-preserving subsets of ontology in DL-Lite[J].Journal of Computer Research and Development,2011,48(12):2334-2342.(in Chinese)

[14]Baader F,Aloza R P N,Suntisrivaraporn B.Pinpointing in the description logic EL[A].Proceedings of the 2007 International Workshop on Description Logics[C].Berlin:Springer,2007.52-67.

[15]Du J,Qi G.Decomposition-based optimization for debugging of inconsistent OWL DL ontologies[A].Proceedings of the 4th International Conference on Knowledge Science,Engineering and Management[C].Berlin:Springer,2010.88-100.

付雪峰 男,江西高安人,1978年出生.南昌工程學(xué)院信息工程學(xué)院講師,主要研究方向:本體調(diào)試與修正,不一致性處理.

E-mail:fxf@seu.edu.cn

漆桂林 男,江西宜豐人,1977年出生.東南大學(xué)計(jì)算科學(xué)與工程學(xué)院教授,博士生導(dǎo)師,主要研究方向:知識(shí)表達(dá),語義網(wǎng),不一致推理等.

E-mail:gqi@seu.edu.cn

張 勇 男,山東蓬萊人,1989年出生.東南大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院碩士研究生,主要研究方向:本體映射與調(diào)試.

E-mail:zhangyong@seu.edu.cn

A Graph-Based Approach for Calculating MinimalUnsatisfiability-Preserving Subsets of Ontology in DL-Lite

FU Xue-feng1,QI Gui-lin2,ZHANG Yong2

(1.SchoolofInformationEngineering,NanchangInstituteofTechnology,Nanchang,Jiangxi330099,China;2.SchoolofComputerScienceandEngineering,SoutheastUniversity,Nanjing,Jiangsu210096,China)

Inconsistency often occurs during ontology evolution,and leads to the invalidity of standard reasoning.Minimal unsatisfiablility-preserving sub-TBox (MUPS) can provide an explanation of the unsatisfiability of a concept in an ontology.Finding all MUPS is an important nonstandard reasoning task in ontology engineering.Most of the approaches for calculating MUPS are built on external description logic reasoners.However,a reasoner-based method can hardly achieve positive efficiency and stability.In this paper,we propose a reasoner-independent approach to calculating MUPS using graph representation.We first transform DL ontologies to graphs,and find MUPS by computing the minimal unsatisfiability-preserving path-pair (MUPP) based on the transformed graphs.We implement and evaluate our approach.The experimental results demonstrate that our approach performs well in efficiency and stability.

ontology;description logic;inconsistency handling;minimal unsatisfiablility-preserving sub-TBox

2015-06-24;

2015-12-03;責(zé)任編輯:覃懷銀

國家“八六三”高技術(shù)研究發(fā)展計(jì)劃基金項(xiàng)目(No.2015AA015406);國家自然科學(xué)基金(No.61272378);江西省教育廳青年科學(xué)基金項(xiàng)目(No.GJJ12643)

TP391

A

0372-2112 (2016)09-2040-06

??學(xué)報(bào)URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.09.002