基于描述邏輯的ODMG對象數(shù)據(jù)模型表示與推理

劉 海，湯 庸，陳啟買

(華南師范大學(xué)計(jì)算機(jī)學(xué)院，廣東廣州510631)

面向?qū)ο髷?shù)據(jù)庫技術(shù)是面向?qū)ο蠹夹g(shù)和數(shù)據(jù)庫技術(shù)結(jié)合的產(chǎn)物．隨著網(wǎng)絡(luò)平臺(tái)模型、移動(dòng)網(wǎng)絡(luò)技術(shù)、場景技術(shù)發(fā)展，業(yè)界存在大量對象數(shù)據(jù)的管理需求．ODMG 組 織 先 后 推 出 ODMG 1．0［1］、ODMG 2．0［2］和 ODMG 3．0［3］規(guī)范，學(xué)者們從面向?qū)ο髷?shù)據(jù)庫的查詢優(yōu)化［4］、面向?qū)ο髷?shù)據(jù)庫管理系統(tǒng)的主動(dòng)機(jī)制［5］和面向?qū)ο髷?shù)據(jù)模型的時(shí)態(tài)擴(kuò)展［6］等方面進(jìn)行相關(guān)研究．與ER數(shù)據(jù)模型、UML軟件功能模型相似，ODMG面向?qū)ο髷?shù)據(jù)模型同樣存在對象一致性、關(guān)系一致性、冗余性判斷問題，因此需要研究ODMG對象數(shù)據(jù)模型的一致性和冗余性等自動(dòng)推理判斷問題．

有關(guān)數(shù)據(jù)模型的相關(guān)檢測的研究，CALVANESE等［7-8］和 BAADER 等［9］分別利用描述邏輯 DLR 和ALNUI，將ER模型轉(zhuǎn)化為描述邏輯DLR和ALNUI的知識(shí)庫，并利用描述邏輯DLR和ALNUI的推理機(jī)制，對ER模型實(shí)體可滿足性、關(guān)系可滿足性和模型冗余性等進(jìn)行自動(dòng)推理，但沒有考慮ER模型中的屬性依賴關(guān)系．LUTZ［10-11］研究了帶屬性依賴的ER模型的自動(dòng)推理問題．蔣運(yùn)承等［12-13］針對模糊數(shù)據(jù)庫的特點(diǎn)，特別是模糊ER模型的驗(yàn)證需求，在描述邏輯ALNUI的基礎(chǔ)上，提出模糊描述邏輯FALNUI，并將模糊ER模型轉(zhuǎn)化為對應(yīng)的知識(shí)庫，利用FALNUI的推理機(jī)制對模糊ER模型進(jìn)行推理;同樣，蔣運(yùn)承等［14］將帶屬性依賴時(shí)序ER模型εRVTAD轉(zhuǎn)化為ALCQI(D)US的知識(shí)庫，從而利用ALCQI(D)US的推理機(jī)制對帶屬性依賴時(shí)序ER模型εRVTAD的可滿足性、冗余性、包含關(guān)系和蘊(yùn)含關(guān)系等問題進(jìn)行自動(dòng)推理．CALVANESE等［15］利用描述邏輯討論面向?qū)ο髷?shù)據(jù)模型與描述邏輯ALUNI知識(shí)庫關(guān)系，并證明對(類)數(shù)據(jù)的包含關(guān)系、可滿足關(guān)系性，但對對象數(shù)據(jù)之間聯(lián)系的依賴關(guān)系缺少深入的研究．BERARDI等［16］研究了UML類圖與描述邏輯知識(shí)庫之間的關(guān)系，利用描述邏輯DLRifd將UML中的類、關(guān)聯(lián)、聚合、繼承等概念或關(guān)系轉(zhuǎn)化為DLRifd知識(shí)庫，通過DLRifd推理能力對UML類圖模型的一致性、包含關(guān)系和等價(jià)問題進(jìn)行自動(dòng)推理，但主要側(cè)重點(diǎn)以對象程序設(shè)計(jì)視角對靜態(tài)類圖及其關(guān)系進(jìn)行知識(shí)表示和推理，因此ODMG面向?qū)ο髷?shù)據(jù)模型知識(shí)表示和相關(guān)問題自動(dòng)推理，是適應(yīng)語義數(shù)據(jù)處理技術(shù)和面向?qū)ο髷?shù)據(jù)模型應(yīng)用發(fā)展的內(nèi)在要求．

本文針對ODMG面向?qū)ο髷?shù)據(jù)模型，在描述邏輯ALCQI(D)的基礎(chǔ)上，將ODMG面向?qū)ο髷?shù)據(jù)庫模型轉(zhuǎn)化為知識(shí)庫，并證明轉(zhuǎn)換正確性．然后借助描述邏輯［17］的推理服務(wù)能力，將ODMG面向?qū)ο髷?shù)據(jù)模型中類一致性、包含性、冗余性檢測問題轉(zhuǎn)化為相應(yīng)知識(shí)庫的推理問題．

1 ODMG對象數(shù)據(jù)模型

對象數(shù)據(jù)庫管理系統(tǒng)通過直接存儲(chǔ)對象來進(jìn)行數(shù)據(jù)管理，對象是面向?qū)ο髷?shù)據(jù)模型的基本構(gòu)造詞，對象狀態(tài)通過其屬性取值體現(xiàn)，也可以是關(guān)系屬性．類與類間可以有繼承關(guān)系．面向?qū)ο驩DMG對象數(shù)據(jù)模型可以用ODL語言描述［5］．為了簡單起見，本文僅考慮ODMG對象數(shù)據(jù)模型的靜態(tài)屬性部分，而不考慮其行為特征．

為了對ODMG面向?qū)ο髷?shù)據(jù)模型進(jìn)行形式化定義，首先對ODMG基本數(shù)據(jù)類型Γ和其類型取值進(jìn)行形式化定義:

定義1［3］ODMG對象數(shù)據(jù)類型OΓ定義為:

ODMG預(yù)先定義的對象類型(如 Object)是ODMG對象數(shù)據(jù)類型，即ROΓ?OΓ．

ODMG對象數(shù)據(jù)模型中的類標(biāo)志符號是ODMG對象類型，即CΓ?OΓ．

定義2［3］ODMG文字?jǐn)?shù)據(jù)類型LΓ定義如下:

預(yù)先定義的文字類型是ODMG文字?jǐn)?shù)據(jù)類型，即 RLΓ?LΓ;

設(shè)l_constr代表一般集合文字類型構(gòu)造詞，代表著{set，bag，list，array}，則對于任意的 ODMG 類型τT，則集合文字構(gòu)詞l_constr＜T＞?LΓ;

設(shè) p1，…，pnAS∪RS是不同的標(biāo)志符，AS為類中屬性成員的集合，RS是類中關(guān)系屬性的集合，并且t1，…，tn是T的類型，則結(jié)構(gòu)文字struct(p1t1，…，pntn)?LΓ．

ODMG對象數(shù)據(jù)類型OΓ和文字?jǐn)?shù)據(jù)類型是ODMG面向?qū)ο髷?shù)據(jù)庫模式中合法的數(shù)據(jù)類型．記作 T=O?！萀Γ．

定義3 假定符號O表示對象數(shù)據(jù)類型OΓ的集合，νO為對象取值論域，νO定義如下:

O?νO．

若 ν1，…，νkνO，則［υ1，…，υk］νO．

若 ν1，…，νkνO，則［A1∶υ1，…，Ak∶υk］νO．

其他均不是νO．

定義4 假設(shè)符號v是文字?jǐn)?shù)據(jù)類型T數(shù)據(jù)的集合，vL是文字對象取值論域，vL定義如下:

v?νL．

若 ν1，…，νkνL，則［υ1，…，υk］νL．

若 ν1，…，νkνL，則［A1∶υ1，…，Ak∶υk］νL．

定義5 給定2個(gè)有限集合X和Y，從X到Y(jié)的函數(shù)如果滿足:?xiX，有 T(xi)=yiY，則稱 T為Y上的X標(biāo)記的元組，并記為T(X，Y)．

下面給出ODMG面向?qū)ο髷?shù)據(jù)庫模型的形式化定義．

定義6 ODMG面向?qū)ο髷?shù)據(jù)庫模式可以刻畫為元組 TS= 〈LS，≤S，≤T，attS，attR〉，其中

(1)LS=CS∪AS∪RS∪TS∪DS，其中 CS是ODMG面向?qū)ο竽Ｐ皖惷柕挠邢藜?AS是類中attribute屬性符號的有限集合，可以是簡單屬性(Simple Attribute)符號，記作 A，也可為結(jié)構(gòu)屬性(Structure Attribute)符號，記為S，每個(gè)屬性Ai都有1個(gè)基本論域BDi;RS是類中relationship關(guān)系屬性符號的有限集合;TS是ODMG面向?qū)ο髷?shù)據(jù)模型中合法數(shù)據(jù)類型的集合，包括ODMG對象數(shù)據(jù)類型OΓ和ODMG文字?jǐn)?shù)據(jù)類型LT;DS是基本論域符號的集合，它們是由文字取值論域νLT、對象取值論域νO和具體論域ΦD組成．

元組(CS，AS，RS，TS，DS)稱為是 ODMG 面向?qū)ο竽Ｐ偷膕ignature．

(2)≤S?CS×CS是CS之間的繼承關(guān)系．

(3)≤T?TS×TS是TS之間的繼承關(guān)系．

(4)attA:CS→T(AS，DS)是從 CS到 T(AS，DS)的函數(shù)，即對類中的任意對象O，attA將對象O映射為DS上的AS標(biāo)記的取值，這個(gè)取值可能是簡單的對象類型，或是文字類型，也可能是集合文字類型，還可以是結(jié)構(gòu)類型．

(5)attR:RN(CS，C'S)→T是ODMG對象模型中2個(gè)對象類型之間關(guān)系取值函數(shù)．這個(gè)取值可能是原子對象類型，或是原子文字類型，還可能是結(jié)構(gòu)類型．

為了刻畫ODMG面向?qū)ο髷?shù)據(jù)模型的語義，引入和對象數(shù)據(jù)模型表示信息結(jié)構(gòu)相一致的面向?qū)ο髷?shù)據(jù)庫狀態(tài)(OODS)．

定義7 ODMG面向?qū)ο髷?shù)據(jù)庫模式S對應(yīng)的數(shù)據(jù)庫實(shí)例 J是1 個(gè)四元組(OS，π，ρ，λ)，其中 OS是由1組有限的對象標(biāo)志符OID集合;函數(shù)π:2OS→CS將OS的子集映射成CS中的某個(gè)類;函數(shù)ρ:OS→νOJ給OS中的指定對象賦值為νOJ．解釋函數(shù)λ:T→ν指定νL的數(shù)據(jù)取值的類型．并且滿足下列條件:

πJ(O)=CJ

λJ(T)=TJ

(l_constr＜T ＞)J={［υ1，…，υk］…，k}}

(Struct(A1:T1，…，Ak:Tk))J={［A1∶υ1，…，Ah∶υh］k，υiTJ

i，i{1，…，k}，υiVoJ，i{k+1，…，h}}．

在這些定義的基礎(chǔ)上，給出ODMG面向?qū)ο髷?shù)據(jù)庫模式S的語義如下:

定義8 給定ODMG對象數(shù)據(jù)庫的模式S，BD=∪DiDSDi是基本論域的集合，并且 Di∩Dj≠?，則OODS=(ΔOB，·OB)是與S對應(yīng)的面向?qū)ο髷?shù)據(jù)庫的狀態(tài)，其中:ΔOB是ODMG面向?qū)ο髷?shù)據(jù)模型使用的基本論域的集合．函數(shù)·OB為:

如果ODMG面向?qū)ο髷?shù)據(jù)庫模式S的狀態(tài)滿足模型中的所有約束，則稱模式S具有的狀態(tài)是可接受的．因而有定義:

定義9 給定ODMG面向?qū)ο髷?shù)據(jù)庫模型S=〈LS，≤S，≤T，attS，attR〉，如果 1 個(gè)面向?qū)ο髷?shù)據(jù)庫狀態(tài) OODS=(ΔOB，·OB)合法，當(dāng)且僅當(dāng) OODS滿足下列條件:

(1)對于模式中存在任意類C，有COB≠?．

(2)對于任意類 C1和 C2，如果 C1≤SC2，則有C1OB?C2OB．

(3)若T是T'的子類，當(dāng)且僅當(dāng)λJ(T)?λJ(T')．

若 attR(C，R)=l_constr＜ C'＞且 attR(C'，R-)=l_constr＜C'＞，則attR是多對多的聯(lián)系，記作R1．

若 attR(C，R)=l_constr ＜ C'＞且 attR(C'，R-)=C，則attR是1對多的聯(lián)系，記作R2．

若 attR(C，R)=C'且 attR(C'，R-)=C，則 attR是1對1的聯(lián)系，記作R3．

2 基于描述邏輯ALCQI(D)的面向?qū)ο髷?shù)據(jù)模型

為了利用描述邏輯的推理機(jī)制對面向?qū)ο髷?shù)據(jù)模型的可滿足性、冗余性和包含關(guān)系等問題進(jìn)行自動(dòng)推理，需要解決2個(gè)問題:(1)將ODMG面向?qū)ο髷?shù)據(jù)模型轉(zhuǎn)化為ALCQI(D)知識(shí)庫，并證明這種轉(zhuǎn)化的正確性;(2)將ODMG面向?qū)ο髷?shù)據(jù)模型的推理問題轉(zhuǎn)化為ALCQI(D)推理問題，同時(shí)證明這種轉(zhuǎn)化的正確性．

2．1 面向?qū)ο髷?shù)據(jù)模型和ALCQI(D)知識(shí)庫轉(zhuǎn)化

與ER模型、UML類圖和知識(shí)庫的對應(yīng)關(guān)系相似，ODMG面向?qū)ο髷?shù)據(jù)庫模式TS與描述邏輯ALCQI(D)知識(shí)庫的對應(yīng)關(guān)系也可以通過轉(zhuǎn)化函數(shù)φ實(shí)現(xiàn)．轉(zhuǎn)化函數(shù)φ需要體現(xiàn)對象數(shù)據(jù)類型和概念之間的關(guān)系．為了描述轉(zhuǎn)化關(guān)系，引入AbstractClass，StruType和LconstrType分別表示類類型、結(jié)構(gòu)體數(shù)據(jù)類型和文字構(gòu)造數(shù)據(jù)類型，Value對應(yīng)于對象類型的取值關(guān)系，member表示文字構(gòu)造類型lconstr-Type中的成員關(guān)系．下面給出轉(zhuǎn)化函數(shù)φ的定義．

定義10 給定1個(gè)ODMG面向?qū)ο髷?shù)據(jù)模型的模式TS，與TS對應(yīng)的描述邏輯ALCQI(D)的知識(shí)庫φ(TS)=(TA，TP，TT)分別由以下規(guī)則得到:

(1)φ(TS)的原子概念集合TA由下列元素組成:·AbstractClass，StruType，LconstrType 是原子概念．

(2)φ(TS)的原子關(guān)系集合TP由下列元素組成:

·member，value為原子關(guān)系．

(3)φ(TS)的公理集合TT由下列元素組成:

Class?=1value．

·對于類C中的不為文字構(gòu)造類型、結(jié)構(gòu)體類型的其他類型屬性a，存在公理:

·若a屬于文字構(gòu)造類型lconstrtType＜T＞，存在公理:

·若a屬于結(jié)構(gòu)類型，存在公理:

·對于對象類C和C'的聯(lián)系屬性R和逆關(guān)系R-，存在如下公理:

φ(R)≡φ(R)-;

φ(R1)≥1φ(R)．φ(C')≥1φ(R')．φ(C)．

φ(R)≡φ(R)-;

φ(R2)≥1φ(R)．φ(C')=1φ(R')．φ(C)．

φ(R)≡φ(R)-;

φ(R3)=1φ(R)．φ(C')=1φ(R')．φ(C)．

·對于類層次關(guān)系，轉(zhuǎn)化為公理:

1)對于extends單繼承關(guān)系，則轉(zhuǎn)化公理為:φ(C1)?value．φ(C2)．

2)對于 ISA多繼承關(guān)系，則轉(zhuǎn)化公理為:φ(C1)?value．(φ(C1)… φ(Ck))．

例1 針對文獻(xiàn)［5］給出的ODMG TS傳化為知識(shí)庫 φ(TS)=(TA，TP，TT)如下:

TA={StruType，SetType，Movie，F(xiàn)ilm，title，year，length，fileType，stars，ownedBy，Star，Addr，Gend，name，address，gender，starredIn，voicein，Stdio，s_name，s_address，owns，Cartoon，voices};

TP={member，title，year，length，filmType，stars，ownedby，name，address，gender，starredIn，voiceIn，s_name，s_address，owns，voices};

(1 Stdio．));

2．2 轉(zhuǎn)化正確性的證明

為了進(jìn)行轉(zhuǎn)化正確性的證明，參照文獻(xiàn)［15］，對ODMG面向?qū)ο髷?shù)據(jù)庫模式TS的深度進(jìn)行定義．

定義11 對于ODMG數(shù)據(jù)模型中任意數(shù)據(jù)類型T的深度dept(T)可以歸納定義如下:

定義12 ODMG面向?qū)ο髷?shù)據(jù)庫模式TS的深度為模式中所有類型表達(dá)式T的深度最大值．

假定TS為ODMG面向?qū)ο髷?shù)據(jù)庫模式，并且深度為m，φ(TS)是轉(zhuǎn)化的 ALCQI(D)知識(shí)庫，I為φ(TS)的有限解釋的論域，記作ΔI|m，為證明定義10轉(zhuǎn)化的正確性，給出如下定理:

定理1 對于任意ODMG面向?qū)ο髷?shù)據(jù)模型TS，存在映射:

(1)αTS是面向?qū)ο髷?shù)據(jù)庫模式TS的實(shí)例J到φ(TS)的有限解釋論域的映射;αv是實(shí)例對象取值到φ(TS)有限解釋論域元素的映射，它們滿足:

對于模式TS的任意實(shí)例J，αTS(J)是φ(TS)的有限解釋論域;

(2)βTS是φ(TS)的有限解釋I的論域到面向?qū)ο髷?shù)據(jù)庫模式TS實(shí)例的映射，βv是φ(TS)有限解釋的論域元素到TS實(shí)例對象取值的映射，它們滿足:

對于φ(TS)的任意有限解釋論域，βTS(I)是面向?qū)ο髷?shù)據(jù)庫模式TS的合法實(shí)例的集合;

對于模式TS中的任意類型T轉(zhuǎn)化得到的φ(T)和論域個(gè)體dΔI|m，如果 d(φ(T))I|m，當(dāng)且僅當(dāng) βv(d)TβT(I)．

證明 (1)ODMG面向?qū)ο髷?shù)據(jù)庫模式TS的數(shù)據(jù)庫實(shí)例J，轉(zhuǎn)換成知識(shí)庫φ(TS)的αTS(J)的解釋如下:

·αv是將數(shù)據(jù)庫實(shí)例J的任意數(shù)據(jù)庫對象映射為知識(shí)庫φ(TS)解釋論域ΔαTS(J)中的個(gè)體．因此ΔαTS(J)是 αv(v)數(shù)據(jù)元素的集合，并且用 Δid，Δstru和Δlconstr表示原子對象、結(jié)構(gòu)對象和構(gòu)造文字集合對象．

·對于每個(gè)原子概念解釋如下:

·對于每個(gè)原子關(guān)系解釋如下:

對于任意類類型取值關(guān)系

(value)αTS(J)={(d1，d2)|(αv-1(d1)，αv-1(d2))ρJ}．

對于每個(gè)集合類型的成員

(member)αTS(J)={(d1，d2)|{d1Δlconstr且 αv-1(d1)=［…，αv-1(d2)…］}．

若屬性成員類型為結(jié)構(gòu)類型 ，

(φ(A))αTS(J)={(d1，d2)|{d1Δstru且 αV-1(d1)=［…，A:αv-1(d2)，…］}．

對于對象之間的聯(lián)系屬性 R，則

(φ(R1))αTS(J)={αv(o)|#αv(o')|(αv(o)，αv(o'))φ(R)αTS(J)，αv(o')(πJ(C'))≥1}∩{αv(o')|#αv(o)|(αv(o')，αv(o))φ(R)αTS(J)，αv(o)(πJ(C'))≥1}．

根據(jù)類型表達(dá)式的結(jié)構(gòu)，采用歸納法給出轉(zhuǎn)換正確性的證明．

(1)對于ODMG面向?qū)ο竽Ｐ蚑S的數(shù)據(jù)類型T，需要證明對于任意活動(dòng)值vVJ，vTJ當(dāng)且僅當(dāng)αv(v)(φ(T))αTS(J)．對T的結(jié)構(gòu)做歸納證明如下:

如果T為結(jié)構(gòu)類型，即T=struct{A1:T1;…;An:Tn}，其轉(zhuǎn)換公式 φ(T)=StruType ?φ(A1)．φ(T1)?=1φ(A1)… ?φ(Ak)．φ(Tk)?=1φ(Ak)，假設(shè)vTJ當(dāng)且僅當(dāng) αv(v)(φ(T))αTS(J)(i{1，2，…，k})成立．

反過來，假設(shè)d=αv(v)(φ(T))αTS(J)，則對于i{1，…，k}，存在惟一的 diΔαTS(J)使得(d，di)(φ(Ai))αTS(J)滿足并且 di(φ(Ti))αTS(J)，根據(jù) αTS定義，有 v=［A1:v1，…，Ah:vh］(h≥k)和 vi=α-1(d)，根據(jù)假設(shè)vTj，有vstruct{A:T;…;viii11Ak:Tk}J．

也可以證明屬性類型為文字構(gòu)造類型的情形．

(2)對于深度為m的有限知識(shí)庫模型φ(s)，定義合法的面向?qū)ο髷?shù)據(jù)庫狀態(tài)βTS(I)如下:

βv是將解釋論域ΔI|m的任意個(gè)體映射為數(shù)據(jù)庫實(shí)例狀態(tài)Vβts(I)的數(shù)據(jù)元素，并且滿足條件:

①如果 Oβts(I)?Vβts(I)是 βv(d)中數(shù)據(jù)元素的集合，必有dAbstractClassI|m．

對于任意類 C，πβts(I)(C)={βV(d)|d(φ(C))I|m}．

ρβts(I)={(o，v)|βV(d1)=o，βV(d2)=v 且(d1，d2)valueI|m}．

λβts(I)={v|v(φ(T)I|m}．

下面首先采用歸納法證明對于任意面向?qū)ο髷?shù)據(jù)模型TS中的數(shù)據(jù)類型T轉(zhuǎn)換的原子概念φ(T)，有對任意dΔI|m，若 d(φ(T))I|m當(dāng)且僅當(dāng) βV(d)

對任意結(jié)構(gòu)數(shù)據(jù)類型 T=Stru(A1:T1，…，Ak:Tk)，轉(zhuǎn)換成知識(shí)庫的對應(yīng)概念為φ(T)=StruType?φ(A1)．φ(T1)?=1φ(A1)… ?φ(Ak)．φ(Tk)?=1φ(Ak)，假設(shè)有 d(φ(Ti))I|m，當(dāng)且僅當(dāng)βV(di)TβiTS(I)時(shí)成立．進(jìn)一步構(gòu)造 βV(d)=［A1:v，…，A:v］(h≥k)，歸納假設(shè)vβ(di)TiβTS(I)有βv(d)TβTS(I)．

反之假設(shè)βV(d)TβTS(I)，即存在結(jié)構(gòu)類型的數(shù)據(jù)庫元素實(shí)例 βV(d)=［A1:v1，…，Ak:vk］(h≥k)且viTβTS(I)，歸納假設(shè)論域個(gè)體 di=βV-1(v)(φ(Ti))I|m(i{1，2，…，k})，根據(jù) βV定義和 dStruTypeI|m及(d，di)(φ(Ai))I|m，由于每個(gè)屬性φ(A)是函數(shù)，所以d(φ(T))I|m．

也可以證明屬性類型為文字構(gòu)造類型的情形．

2．3 ODMG面向?qū)ο髷?shù)據(jù)模型的推理

ODMG面向?qū)ο髷?shù)據(jù)模型的推理主要包括對象類型(類)的一致性、對象類型(類)包含、對象類型(類)等價(jià)和模式蘊(yùn)含等推理問題．一般情況下，面向?qū)ο髷?shù)據(jù)模型設(shè)計(jì)者需要通過手工對上述問題進(jìn)行檢測，但此方法存在推理效率和可靠性不高的缺點(diǎn)，完備性也得不到保證．下面首先給出ODMG面向?qū)ο髷?shù)據(jù)模型的可滿足性、包含關(guān)系、冗余性和蘊(yùn)含關(guān)系的定義，然后對其推理正確性給出證明．

定義13 給定1個(gè)ODMG面向?qū)ο髷?shù)據(jù)模型TS，C，C1，C2TS，存在1個(gè)合法的面向?qū)ο髷?shù)據(jù)庫的狀態(tài) OODS=(ΔOB，·OB)．

(1)如果π(C)≠?，則稱類C是可滿足的 (類可滿足性);

(2)如果π(C1)?π(C2)，則稱類C2包含類C1;

(3)如果C1?C2和C2?C1都成立，則稱TS存在冗余;

(4)給定1個(gè)面向?qū)ο髷?shù)據(jù)庫模型TS'，并且TS和TS'有著相同的Signature，如果對TS的任意合法的數(shù)據(jù)庫狀態(tài)J，J也是TS'的合法數(shù)據(jù)庫狀態(tài)，則稱TS 蘊(yùn)含 TS'，記作 TS TS'．

下面給出類可滿足性和類包含關(guān)系，模式冗余關(guān)系，模式蘊(yùn)含的有關(guān)轉(zhuǎn)化定理．

證明 先證明“?”．因?yàn)轭怌是可滿足的，所以存在1個(gè)合法的面向?qū)ο髷?shù)據(jù)庫狀態(tài)OODS=(ΔOB，·OB)，使得 π(C)≠?．由定理 1 可知，αTS(OODS)是φ(OODS)的1個(gè)模型，并且有π(C)=(φ(C))αTS(OODS)成立．因?yàn)?π(C)≠?，所以(φ(C))αTS(OODS)≠?，從而有 φ(OODS)?/ φ(C)⊥．

定理3 對于1個(gè)ODMG面向?qū)ο髷?shù)據(jù)模型TS，C1，C2CS是TS中的類，φ(TS)是通過轉(zhuǎn)化規(guī)則得到的ALCQI(D)的知識(shí)庫，則C1≦SC2，當(dāng)且僅當(dāng) φ(TS)?φ(C1)φ(C2)．

證明 首先證明“?”．假設(shè) φ(TS)?/φ(C1)φ(C2)，則 φ(TS)存在1個(gè)模型I，使得o(φ(C1))I和o(φ(C2))I成立，其中 oΔI．再由定理 1 可得，βOODS(I)是1個(gè)合法的面向?qū)ο髷?shù)據(jù)庫狀態(tài)OODS，并 且 有 (φ (C1))I= πβOODS(I)(C1)和(φ(C2))I=πβOODS(I)(C2)成立．由 o(φ(C1))I和o(φ(C2))I可知，C1≦SC2不成立，這與 C1≦SC2矛盾．所以 φ(TS)?/φ(C1)?φ(C2)．

再證明“?”．假設(shè)C1≦SC2不成立，則存在1個(gè)合法的面向數(shù)據(jù)庫的狀態(tài)OODS和1個(gè)對象實(shí)例o，使得 oπ(C1)和 oπ(C2)．由定理1可知，αTS(OODS)是 φ(TS)的 1個(gè)模型 I，且 π(C1)(φ(C1))αTS(OODS)，π(C2)(φ(C2))αTS(OODS)．由 oπ(C1)和 oπ(C2)可知，o(φ(C1))αTS(OODS)和o

這與 φ(TS)?φ(C1)φ(C2)矛盾．所以 C1≦SC2．證畢．

定理4 對于1個(gè)ODMG面向?qū)ο髷?shù)據(jù)模型TS，存在2個(gè)類C1，C2CS，使得C1≦SC2且C2≦SC1成立，φ(TS)是TS通過轉(zhuǎn)化得到的ALCQI(D)的知識(shí)庫，則TS是冗余的，當(dāng)且僅當(dāng)

證明 首先證明“?”．由于TS是冗余的，可知存在2個(gè)類C1，C2CS，使得 C1≦SC2且 C2≦SC1成立．根據(jù)定理1可知，φ(TS)?φ(C1)φ(C2)和φ(TS)?φ(C2)φ(C1)成立．

再證“?”．如果 φ(TS)?φ(C1)φ(C2)和φ(TS)?φ(C2)φ(C1)成立，則根據(jù)定義7可知，C1≦SC2且C2≦SC1成立，從而TS是冗余的．證畢．

定理5 給定2個(gè)ODMG面向?qū)ο髷?shù)據(jù)模型TS和 TS'，φ(TS)和 φ(TS')分別是 TS和 TS'通過轉(zhuǎn)化得到的ALCQI(D)知識(shí)庫，則TS?TS'，當(dāng)且僅當(dāng)φ(TS)?φ(TS')．

證明 首先證明“?”．對于任意的面向?qū)ο髷?shù)據(jù)庫狀態(tài)OODS=(ΔOB，·OB)，由定理2 知，αTS(OODS)是φ(TS)的1個(gè)模型．由TS?TS'知，OODS也是 TS'的合法的面向?qū)ο髷?shù)據(jù)庫狀態(tài)，從而由定理2知，αTS(OODS)也是 φ(TS')的模型．因此有 φ(TS)?φ(TS')．

再證“?”．對于φ(TS)的任意模型I，由定義5知，βOODS(I)是TS的1個(gè)合法的面向?qū)ο髷?shù)據(jù)庫的狀態(tài)．由 φ(TS)?φ(TS')知，βOODS(I)是φ(TS')的1個(gè)模型．由定義4知，βOODS(I)是1個(gè)合法的面向?qū)ο髷?shù)據(jù)庫的狀態(tài)．因此有TS?TS'．證畢．

例2 為了說明ODMG對象數(shù)據(jù)模型的自動(dòng)推理問題，在文獻(xiàn)［5］基礎(chǔ)上，設(shè)計(jì)1個(gè)動(dòng)畫片公司類，用ODL語言描述對象數(shù)據(jù)模型如下:

(1)根據(jù)定義10的轉(zhuǎn)化規(guī)則，在例1產(chǎn)生的知識(shí)庫增加1條公理:

(2)利用以上公理及例1知識(shí)庫中的公理:cartoonmovie，利用描述邏輯的推理機(jī)制，可以發(fā)現(xiàn)AnimationCompany和stdi之間存在如下關(guān)系，即An-imationCompanystdi．從而發(fā)現(xiàn)了數(shù)據(jù)庫模式中潛在的對象類層次關(guān)系(定理3)．

3 小結(jié)

針對面向?qū)ο髷?shù)據(jù)庫的特點(diǎn)，結(jié)合ODMG面向?qū)ο髷?shù)據(jù)模型的自動(dòng)驗(yàn)證需求，在 CALVANESE等［7-8］的工作基礎(chǔ)上，本文將ODMG面向?qū)ο髷?shù)據(jù)模型轉(zhuǎn)化成基于描述邏輯 ALCQI(D)知識(shí)庫，將ODMG面向?qū)ο髷?shù)據(jù)模型的可滿足性、包含關(guān)系、冗余性、蘊(yùn)含性等檢測問題進(jìn)行轉(zhuǎn)化為知識(shí)庫推理服務(wù)，并都給出其正確性證明．未來工作是開發(fā)ODMG TS的知識(shí)庫轉(zhuǎn)化工具和自動(dòng)推理工具，自動(dòng)完成對象數(shù)據(jù)模型相關(guān)自動(dòng)驗(yàn)證．

［1］CATTEL R．The object database standard:ODMG-93［M］．Michigan:Morgan-Kaufmann，1996．

［2］CATTEL R．The object database standard:ODMG 2．0［M］．Michigan:Morgan-Kaufmann，1997．

［3］CATTELL R GG，BARRY D K，BERLERM．The object database standard:ODMG 3．0［M］．Michigan:Morgan-Kaufmann，2000．

［4］GRANT J，GRYZ J，MINKER J，et al．Logic-based query optimization for object databases［J］．IEEE Transactions on Knowledge and Data Engineering，2007，12(4)，529-547．

［5］BERTINO E，GUERRINIG，MERLO I．Extending the ODMG objectmodel with triggers［J］．IEEE Transactions on Knowledge and Data Engineering，2004，16(2):170-188．

［6］BERTINO E，F(xiàn)ERRARIE，GUERRINIG，et al．Extending the ODMG object model with time［C］∥JUL E．Proceedings of the twelfth European Conference on Object-Oriented Programming，Lecture Notes in Computer Science，Berlin:Springer，1998，1445:41-66．

［7］CALVANESE D，LENZERINIM，NARDID．Description logics for conceptual datamodeling［M］∥CHOMICKI J，SAAKEG．Logics for Databases and InformationSystems．Norwell， Massachusetts:Kluwer Academic Publisher，1998:229-264．

［8］CALVANESE D，LENZERINI M，NARDI D．Unifying class-based representaion formalisms［J］．Journal of Artificial Intelligence Research，1999，11:199-240．

［9］BAADER F，HORROCKES I，SCATTLER U．Description logics［M］∥STAAB S，STUDER R．Handbook on Ontologies．Berlin:Springer，2004:3-28．

［10］LUTZ C．Reasoning about entity relationship diagrams with complex attribute dependencies［C］∥Proceedings of the 2002 International Workshop on Description Logics．Toulouse，F(xiàn)rance，2002．

［11］LUTZ C．Reasoning about entity relationship diagrams with complex attribute dependencies［C］∥Proceedings of the 2002 International Workshop on Description Logics．Toulouse，F(xiàn)rance，2002．

［12］蔣運(yùn)承，湯庸，王駒．基于描述邏輯的模糊ER模型［J］．軟件學(xué)報(bào)，2006，17(1)20-30．

［13］蔣運(yùn)承，湯庸，王駒，等．模糊描述邏輯FALNUI的tableaux推理［J］．計(jì)算機(jī)研究與發(fā)展，2007，44(8):1309-1316．

［14］蔣運(yùn)承，湯庸，王駒，等．基于描述邏輯的帶屬性依賴時(shí)序ER模型［J］．計(jì)算機(jī)研究與發(fā)展，2007，44(10):1765-1773．

［15］CALVANESE D，LENZERINIM，NARDID．Unifying class-based representaion formalisms［J］．Journal of Artificial Intelligence Research，1999，11:199-240．

［16］BERARDID，CALVANESE D，GIACOMO GD．Reasoning on UML class diagram［J］．Artifical Intelligence，2005，168:70-118

［17］BAADER F，CALVANESE D，MCGUINNESSD L，et al．The descriptionLogic handbook:Theory，implementation and applications［M］．2th ed．Cambridge:Cambridge University Press，2007．