趙曉非 史忠植 馮志勇
1(天津工業大學計算機科學與軟件學院 天津 300387) 2(中國科學院計算技術研究所智能信息處理重點實驗室 北京 100190) 3(天津大學計算機科學與技術學院 天津 300072)
在信息集成、服務集成以及語義Web等大量的分布式應用中,人們常希望本體是分塊的或分布式的,而不是單一的本體;大規模本體的模塊化具有更強的針對性、更高的推理效率[1].上述2個原因使得分布式、模塊化本體[2-3]成為近幾年的研究熱點之一.多種的邏輯基礎被相繼提出,如ε-連接框架[4]、保守擴展的分布式本體框架[5]、分布式一階邏輯[6]以及基于包的描述邏輯等.作為其中的一個重要的研究分支,分布式動態描述邏輯(distributed dynamic description logics, D3L)[7]引入了語義映射的描述機制、本體間知識的傳播機制以及面向分布式環境的推理機制.D3L很好地滿足了每個局部信息系統希望保持一定程度的自治及自己的用戶界面而從其他局部信息系統導入和重用知識的需求,因而為上述應用提供了較完備的邏輯基礎.
本體間元素的映射和推理是模塊化本體要解決的核心問題.由于現實世界中語義映射的多樣性,其邏輯基礎必須能夠建模異構元素之間的映射并進行推理.不幸的是,現有的研究對此均沒有提供足夠的支持.以ε-連接框架為例,盡管該框架提供了基于消解的分布式推理算法,但通過ε-連接構造的映射僅限于不同本體的概念之間,因而無法實現異構元素之間的映射和推理.保守擴展的分布式本體框架所提供的推理僅適用于本體之間具有簽名依賴性的情形,不符合改約束條件的映射均無法被描述和推理,并且該框架僅從理論上證明了簽名依賴性問題是可判定的,并沒有提供推理算法.

鑒于此,本文將研究擴展到了被包含端存在復合元素的異構橋規則情況下的D3L推理問題.由于分布式Tbox是D3L知識庫最基本的形式,為了獲得分布式Tbox的可判定性,首先給出了其正則性的定義.而后針對將動態描述邏輯DSROIQ作為局部本體語言的D3L知識庫,通過對橋規則進行必要的形式變換以及區分不同情形轉換為已有的語言機制,提出了將分布式知識庫轉換為單一DSROIQ知識庫的算法.接著我們對轉換算法的性質進行了研究.證明了算法可以在多項式時間內終止、算法的目標知識庫與原始知識庫在可滿足性上是等價的,進而證明了在上述橋規則存在的情況下正則D3L知識庫的集中式推理具有與單一DSROIQ知識庫推理相同的最壞時間復雜度.本文的算法使得D3L推理可以獲得與現有的分布式推理算法相同的最壞時間復雜度并且解決了后者難以處理異構復合橋規則的問題.

Fig. 1 Sample for heterogeneous composite bridge rules圖1 異構復合橋規則示例
限于篇幅,在此僅對與本文聯系密切的D3L 相關部分進行簡要闡述,更詳細的信息請參考文獻[8].首先介紹動態描述邏輯DSROIQ中的概念、角色和動作,然后介紹DSROIQ之上的分布式知識庫及其解釋的相關知識.
定義1. DSROIQ的概念是下述情形之一的表達式:

其中,A表示原子概念;C,D表示普通概念;a表示個體;R,S表示角色;n為正整數.
DSROIQ允許角色之間進行2種運算:連接運算和逆運算.R°S表示角色R和S的連接;而S-表示角色S的逆.DSROIQ的角色包含公理(RIA)是形如S1°S2°…°SnR的表達式.RIA的集合可以構成角色層次.給定局部TboxTB以及個體t,u,從t到u的路徑是角色的1個非空序列R1(x1,x2),R2(x2,x3),…,Rn(xn,xn+1)∈TB,其中x1=t,xn+1=u且xi≠xi+1,1≤i≤n.如果不存在起始于個體t的路徑,則稱t為終端;如果不存在終止于個體t的路徑,則稱t為始端.
定義2. 如果1個角色層次中的角色之間存在滿足2個條件的偏序關系:
1)SR當且僅當S-R;
2) 每個RIA是滿足SiR,i=1,2,…,n的下列表達式之一:R°RR,R-R,S1°S2°…°SnR,R°S1°S2°…°SnR,S1°S2°…°Sn°RR,則稱該角色層次是正則的.
定義3. DSROIQ的原子動作α=(P,E)定義如下:
1)α為原子動作名;
2)P是由公理組成的有限集合,表示動作執行前必須滿足的前提條件;
3)E是由公理組成的有限集合,表示執行該動作后將會發生的影響.
D3L知識庫[9]的最基本形式——分布式Tbox由局部Tbox的集合和提供局部Tbox之間映射的橋規則的集合構成,每個局部Tbox建立在獨立的動態描述邏輯語言之上.DSROIQ之上的分布式Tbox的定義如下:





分布式TboxDTB的1個解釋I={Ii}i∈I,{ri j}i,j∈I,i≠j,其中{Ii}i∈I是局部解釋的集合,{ri j}i,j∈I,i≠j是領域關系的集合.對于每個i∈I,有每個領域關系ri j是的子集且有ri j(d)={d′|d,d′∈ri j}.
定義5. 解釋I滿足分布式TboxDTB中的元素或公理(記為I·),當且僅當I滿足11種情形(i,j∈I):
10)DTBi:CD,如果對任意解釋I,IDTB成立蘊含Ii:CD成立;
11)DTBi:RS,如果對任意解釋I,IDTB成立蘊含Ii:RS成立.

Fig. 2 Sample for the regularity of distributed Tbox圖2 分布式Tbox的正則性示例
Horrocks等人[10]對SROIQ進行了系統的研究,發現SROIQ的正則Tbox——即僅允許存在正則角色層次的Tbox——的基本推理問題是可判定的.引入動作理論之后,Chang等人[11]的研究表明動作理論的引入并不改變原有描述邏輯推理問題的可判定性.為了獲得以DSROIQ作為局部本體語言的DTB的可判定性,我們對定義2進行擴展,得到分布式Tbox正則性的定義.
定義6. 如果1個分布式TboxDTB的角色層次中的角色之間存在滿足3個條件的偏序關系:
1)SR當且僅當S-R;
2) 每個RIA是滿足SiR,i=1,2,…,n的下列表達式之一:R°RR,R-R,S1°S2°…°SnR,R°S1°S2°…°SnR,S1°S2°…°Sn°RR;
①v到y不存在路徑;
②SR;
③S=R(即B中存在R(z,v)),但不存在R(z′,v′)滿足v′到y之間有路徑,且若x=z則B中不存在C(x),若y=v則B中不存在C(y),
則稱該分布式TboxDTB是正則的.

有關正則性更詳細的信息請參閱形式語言與自動機的相關知識.


步驟1. 初始化B′=B;
步驟2. 對于B′中每個變元x,令{C1(x),C2(x),…,Cn(x)}代表B′中所有引用x的概念公理的集合,迭代計算B′=B′{C1(x),C2(x),…,Cn(x)}∪{(C1C2…Cn)(x)};

步驟1~3在每次迭代過程中對B′中的角色公理的數目進行約簡,顯然會在有限步驟內結束,而且迭代過程結束后,B′中所有路徑的終端個體只能是作為H中角色公理的第2個參數出現的個體,因此所有路徑都終止于該終端個體.如果H=C(x)則按照上述步驟,所有路徑都已被約簡去除,因此B′中不存在任何路徑.

證畢.
以橋規則worksAt(x,y)University(y)supervises(x,z)PhDStudent(z)profOf(x,z)為例,其中B=worksAt(x,y)University(y)supervises(x,z)PhDStudent(z)經過轉換,得到的B′=?worksAt.University(x)supervises(x,z)PhDStudent(z),其中z為單一的最大路徑的終端.
由于橋規則本質上描述的是跨本體的包含關系,因此盡管定理1針對的是into-橋規則的情形,對于onto-橋規則同樣有類似的結果,可對被包含端進行同樣的轉換,其證明思路與定理1類似,此處不再贅述.
根據定理1可知,復合橋規則的角色路徑均可等價轉換為單一的線性路徑,其中每個個體變元均屬于該最大路徑的一部分.文中我們假定所處理的橋規則均具有定理1等價變換后的形式.
在定理1的基礎上,通過全面考慮構成異構復合橋規則的不同形式,我們研究了異構復合橋規則的轉換語義并給出了分布式知識庫的轉換算法.該算法可以將DSROIQ作為局部本體語言的D3L知識庫轉換為單一的DSROIQ知識庫.
算法1. D3L知識庫的轉換算法.
輸入:以DSROIQ作為局部本體語言的分布式知識庫DTB:{Ti}i∈I,BR;
輸出:單一的DSROIQ知識庫TBBR.
步驟1. 初始化TBBR=?,初始化剩余橋規則的集合BR′=BR;
步驟2. 若BR′=?,則令TBBR=TBBR∪{Ti}i∈I,輸出TBBR,算法結束;

步驟4. 分5種情形判斷:
1) 若B中存在引用同1個體變元z的2個概念公理D(z)和D′(z),則將兩者從B中刪除并將(DD′)(z)加入B中;
2) 若H=C(x)且B=D(x),則將該橋規則從BR′中刪除并將DC加入TBBR;
3) 若H=R(x,y)且B形如{R1(x,x2),R2(x2,x3),…,Rn(xn,y)},則將該橋規則從BR′中刪除并將R1°R2°…°RnR加入TBBR;
4) 若H=R(x,y)且B中存在D(z)滿足z出現在B或H的角色公理(第1參數或第2參數均可)中,則執行3步驟:
① 引入新角色S,將D=?S.Self加入TBBR;
② 引入新變元z′,將角色公理S(z,z′)加入B,將每個角色公理T(x′,z)∈B替換為T(x′,z′),將每個角色公理T(z,y′)∈B替換為T(z′,y′);
③ 將D(z)從B中刪除,若z=y則將H替換為R(x,z′);
5) 若H=C(x)或H=R(x,y)且B中存在D(z)滿足z既不出現在H中也不出現在B的任意角色公理中,則執行2步驟:
① 引入新變元u,若存在R(x,t)∈B則令u=y,否則令u=x;
② 將B中D(z)替換為?U.D(u),其中U為全局角色;
步驟5. 跳轉到步驟2.
算法1從剩余橋規則的集合BR′中依次取出橋規則進行處理,直至BR′為空,算法1終止.在處理每條橋規則的過程中,分5種情形處理.其中橋規則經過情形1、情形4和情形5進行轉換和約簡,直到滿足情形2或情形3時被最終從BR′中刪除.下面我們分析一下這5種情形是否涵蓋了所有可能的情況.我們可以通過橋規則的形式若不滿足情形1~4,則必然滿足情形5的思路來進行證明.假定情形1~4的前提條件均不滿足,由于橋規則的包含端為非復合元素,因此H無外乎2種情況:H=C(x)或H=R(x,y).如果H=C(x),根據定理1可知B中不存在角色公理,即B中只能是概念公理.由于情形2的前提條件不滿足,即B不是D(x)的形式,則必有D(z)∈B存在,且z既不出現在H中也不出現在B的任意角色公理中,情形5的前提得以滿足.如果H=R(x,y),根據定理1可知B中的所有路徑均被包含于1個單一的最大路徑中且y是該最大路徑的終端.由于情形3的前提條件不滿足,即B不具備R1(x,o1),R2(o1,o2),…,Rn-1(on-2,on-1),Rn(on-1,y)的形式,因此必有概念公理D(z)∈B存在.再根據假設,情形4的前提條件不滿足,也就是z不出現在B和H的角色公理中,因此情形5的前提條件得以滿足.通過上述分析可知,無論H=C(x)或H=R(x,y),如果橋規則的形式不滿足情形1~4,則必然滿足情形5,因此算法所區分的5種情形涵蓋了所有可能的情況.
下面通過實例對算法的執行加以說明.以2.2節中的橋規則為例,詳細的中間結果列于表1中.經過算法1的轉換,最終可得3條DSROIQ公理(其中S1,S2為新引入的輔助角色):S1°supervises°S2profOf;?worksAt.University≡?S1.Self;PhDStudent≡?S2.Self.

Table 1 Sample for the Transformation of Bridge Rules表1 橋規則轉換示例
下面我們對算法1的性質以及復雜橋規則情況下D3L集中式推理的計算復雜度問題進行研究.定理2闡述了算法1的時間復雜度問題.定理3闡述了算法1輸出的目標知識庫TBBR與原始知識庫DTB在可滿足性上是等價的.定理4闡述了DTB的正則性與TBBR正則性的關系,進而證明了復合橋規則存在的情況下D3L的集中式推理具有與單一DSROIQ知識庫推理相同的最壞時間復雜度.
定理2. 算法1將在多項式時間內終止.
證明. 顯然算法1的單個步驟均可在線性時間內完成,因此對算法總體時間復雜度有影響的只有每個步驟執行的次數.下面對每步所執行的次數進行分析.步驟1~3可以在多項式數目步驟內完成,我們主要分析步驟4.情形1和情形4約簡了橋規則中概念公理的個數.由于在約簡過程中并不引入新的概念公理,因此對于每個概念公理,無論是情形1或情形4至多執行1次.情形2~3約簡了橋規則的個數,同樣可以在多項式步驟數內結束.情形5約簡了概念公理的個數,這些公理不存在出現在橋規則的包含端中的個體變元.由于在情形5的執行過程中并不引入此種概念公理因此可以在多項式步驟數內結束.
綜上所述,算法1將在多項式時間內終止.
證畢.
定理3. 算法1輸出的知識庫TBBR與DTB具有相同的可滿足性.
證明. 要證明TBBR與DTB具有相同的可滿足性,可以歸納地證明算法的每步轉換都不改變可滿足性即可.令TB0BR0和TB1BR1分別代表1個轉換步驟執行之前和之后的TBBRBR′,我們需要證明TB∪TB0∪BR0和TB∪TB1∪BR1具有相同的可滿足性.
情形1~3均為等價替換,不會改變轉換前后的知識庫可滿足性.

反過來,若TB∪TB1∪BR1是可滿足的(即存在解釋ITB∪TB1∪BR1),我們來證明TB∪TB1∪BR0也是可滿足的.根據假設可知對于任意變元賦值π均有(B1H1)I,π為真.與前面類似,我們只需考慮為真的情況即可.令π′表示π′(z′)=π(z),π′(x)=π(x)(當x≠z′時)的變元賦值,很顯然為真,考慮到假設條件(B1H1)I,π′為真可知為真,因此有為真.對于在H0中出現的所有變元,π′與π均相同,因此為真,進而IB0H0.最終可得ITB∪TB1∪BR0成立,即TB∪TB1∪BR0是可滿足的.
綜上,情形4不改變轉換前后的知識庫可滿足性.



通過上述分析可知,算法1的每步轉換均不改變知識庫的可滿足性,因此TBBR與DTB具有相同的可滿足性.
證畢.
定理4. 若DTB是正則的,則算法1輸出的知識庫TBBR也是正則的.
證明. 我們只需證明算法1的每步轉換都不改變知識庫的正則性即可.

對于情形4,若新引入的角色S先序于H中的角色R(x,y)且S為B中的單一最大路徑帶來新的始端元素替換了先前作為路徑起始的R(s,t)中的始端s,或者S為B中的單一最大路徑帶來新的終端元素替換了先前作為路徑終點的R(s,t)中的終端t,只有這2種情況下知識庫的正則性才有可能被改變,然而根據情形4的前提條件可知,在上述情況下被約簡的概念公理D(z)只能是D(x)或D(y)兩者之一,因此S的引入都不會改變正則性.
情形5與情形4類似,僅當R中的第1個個體變元構成B的單一最大路徑的始端或第2個個體變元構成單一最大路徑的終端時,?U.D(u)的引入才有可能改變知識庫的正則性.在第1種情況下,我們令u=y(參見情形5的步驟①),此時u并沒有替換先前的最大路徑的始端,因此正則性并沒有被改變;在第2種情況下,我們令u=x,此時u并沒有替換先前的最大路徑的終端,正則性仍然得以保持.
證畢.
如2.1節所述,檢測正則DSROIQ知識庫的可滿足性問題是可判定的,因此根據定理4可知,若DTB是正則的,則TBBR也是正則的,即檢測TBBR的可滿足性問題是可判定的.再考慮定理3TBBR與DTB具有相同的可滿足性可知檢測DTB的可滿足性問題是可判定的.考慮到橋規則集合可以在多項式時間內轉換為DSROIQ公理(定理2),可得該問題的最壞時間復雜度與檢測TBBR的可滿足性問題的最壞時間復雜度相同.最終我們可以得到定理5.
定理5. 給定DSROIQ作為局部本體語言的分布式TboxDTB,必存在單一的DSROIQ TboxTBBR滿足TBBR可以在BR規模的多項式時間內被計算出來且TBBR與DTB具有相同的可滿足性.若DTB是正則的,則檢測DTB的可滿足性問題是可判定的,且其最壞時間復雜度與檢測TBBR的相同.
針對復雜的分布式本體系統邏輯基礎的研究,國內外研究人員提出了不同的思路和方法,包括基于ε-連接的描述邏輯、分布式動態描述邏輯、基于保守擴展的分布式本體框架、分布式一階邏輯等.下面對這些研究進行對比分析.
Grau等人[4]和Mossakowski等人[12]提出了一種分布式本體框架,該框架使用ε-連接對各個本體進行組合.利用連接來描述本體間的外化關系,隨后將連接應用于存在性限定和值限定可以構造跨越本體的復雜概念(例如利用連接E∈εi j和Tj中的概念C可以構造Ti中的概念?E.C,其中εi j是Ti和Tj之間有向連接的集合).文獻[13]對該框架進行了模態化擴展并引入了一系列消解推理規則,為其提出了基于消解的分布式推理算法.ε-連接框架僅對復雜概念之間的語義映射提供了一定的支持,并且其前提條件要求局部領域必須是互不相交的,而此特點就決定了它并不適合于作為語義Web這樣的局部異構而又部分交疊的系統的邏輯基礎.此外,為了滿足局部領域的互不相交性還需要對該框架的表達能力進行多種限制,比如1個本體中的元素不能聲明為其他本體中元素的子元素超元素,因而該框架無法實現包含關系在不同本體之間的傳播.盡管在局部本體組合和推理方面該框架解決得較好,與D3L相比,ε-連接框架的描述能力和知識傳播能力較有限.
文獻[14]對D3L中橋規則的屬性及其導致的知識傳播進行了研究.通過在D3L解釋中的領域關系之上引入組合一致性語義解決了包含關系無法在局部本體間正確傳播的問題.證明了該語義不改變D3L的原始屬性.為擴展后的D3L提出了分布式Tableaux推理算法并證明了該算法是可終止的、可靠的和完備的.文獻[7]引入了合取映射橋規則,解決了橋規則包含合取元素時包含關系無法正確傳播的問題,在此基礎上提出了合取映射橋規則到普通橋規則的轉換方法并證明了方法的正確性,從而可將帶上述橋規則的D3L的推理問題轉化為傳統的推理問題.然而上述研究僅針對包含原子元素的同構橋規則,對于包含復合元素的異構橋規則的更一般情形則并沒有涉及到,而且所提出的分布式Tableaux推理算法是采用局部本體推理加消息傳遞的機制實現的,其時間復雜度與單一本體的推理相比并沒有明顯的優勢.
Lutz等人[5]提出的分布式本體框架使用保守擴展來描述本體之間的聯系.本體T1∪T2是本體T1關于簽名Σ的1個保守擴展當且僅當T1∪T2關于Σ的每個邏輯結論也是T1的邏輯結論.他們針對多種主流描述邏輯(ALC,ALCQI,ALCQIO,EL)研究了判定該問題以及2個本體之間的簽名依賴性問題的可判定性及其推理復雜度.文獻[15-16]進一步為該框架引入了模型論語義并研究了相關的推理問題.基于保守擴展的框架不僅可用于分布式本體的集成,也可用于將單個本體分解為不同的模塊.然而與D3L相比,該框架的適用性局限于分布式本體之間具有簽名依賴性的情形,不符合該約束條件的復合元素之間的映射均不被支持.我們認為過于嚴格的限制條件降低了該框架對分布式特性的描述和推理能力,并且該框架僅從理論上證明了簽名依賴性問題是可判定的,并沒有提供本體推理算法.
此外,基于對傳統分布式一階邏輯(DFOL)的語義映射機制進行擴展,Chiara等人[6]提出了修訂版的分布式一階邏輯.盡管具有較強的描述能力并證明了定理證明方法是完備的和可靠的,然而該框架僅提供的是自然演繹推理的定理證明方式,因此距實際問題中的高效應用尚有一定距離.
本文研究了被包含端存在復合元素的異構橋規則情況下的D3L推理問題.通過擴展角色層次正則性的定義,我們定義了DTB的正則性,提出了將描述邏輯DSROIQ作為局部本體語言的D3L知識庫轉換為單一DSROIQ知識庫的算法,接著研究了算法的性質以及基于該轉換的D3L集中式推理的復雜度的相關問題.本文的研究能夠有效處理異構復合橋規則,并且表明支持此種橋規則的D3L集中式推理可以獲得與現有D3L分布式推理算法相同的最壞時間復雜度.
未來的工作包括將該研究推廣到EL,EL++作為局部本體語言的D3L,研究橋規則轉換的可能性及方法、分析其復雜度并開發相應的推理機等.