描述逻辑(description logic)是一簇知识表示的语言,其以结构化、形式化的方法来表示特定应用领域的知识.作为一类用于知识表示的形式化工具,描述逻辑在信息系统、软件工程以及自然语言处理等领域得到了广泛的应用^[1].特别是在第三代Web——语义网(semantic Web)中,描述逻辑更是扮演着关键角色,并成为W3C推荐Web本体语言OWL的逻辑基础^[2].

表达能力(expressive power)和推理复杂性(complexity of reasoning)是一个逻辑的两个重要特征,也是一对相互制约的关系.一般而言,表达能力越强,其推理的复杂性越高;反之,表达能力越弱,其推理的复杂性也就越低.目前,对描述逻辑的推理复杂性的研究已经取得了较为丰硕的成果,比如文献[3,4,5,6,7,8],而对其表达能力的研究则相对较少.描述逻辑及其扩展(以下简称族)是一类重要的知识表示语言.例如,盖伦医疗知识库(Galen medical knowledge base,简称GALEN)^[9]和美国国家癌症研究所(national cancer institute,简称NCI)^[10]的癌症知识库,都是以族作为它们的表示语言基础.因此,开展对描述逻辑族表达能力的研究,不仅能够为寻求表达能力与推理复杂性之间的平衡关系,而且也能为医学知识库构建中逻辑语言的选择提供有益的支持和帮助.

一个逻辑的表达能力可以从以下的3个角度来分析^[11]:

(1) 给定一个逻辑,什么样的符号串是该逻辑的公式(well-formed formula);

(2) 一个逻辑公式的语义解释;

(3) 构建一个逻辑到另一个逻辑的翻译,然后比较它们的相对表达能力.

本文侧重从上面第3个角度来分析一个逻辑的表达能力.解释之间的互模拟(bisimulation)关系是从语义的角度刻画逻辑表达能力的一个有效途径,其代表性的结果是命题模态逻辑(modal logic)表达能力的刻画定 理——van Benthem刻画定理^{[12, 13]}:假定一阶逻辑的语言仅包含1个二元关系符号和一元谓词符号,那么一阶公式a(x)等价于某个命题模态逻辑公式在标准关系翻译(standard relational translation)下的公式,当且仅当该公式的可满足性在互模拟关系下被保持.上述结果精确地刻画了一阶逻辑公式与命题模态逻辑公式等价的充分必要条件.

描述逻辑是一类逻辑,其基本语法对象是概念名(concept name)、角色名(role name)以及个体名(individual name).通过构造子集合,由概念名和角色名来构建复杂的概念;然后,在概念的基础上形成术语公理集(terminological axiom box,简称TBox).由此,描述逻辑的表达能力刻画可以分为2层:概念的表达能力和术语公理集的表达能力.由于许多描述逻辑都能翻译到一阶逻辑不同的子部分(fragment),所以刻画描述逻辑系统表达能力的一个途径是:首先,构建描述逻辑到一阶逻辑翻译;然后,给出描述逻辑解释之间的模拟关系,建立类似van Benthem刻画定理的结论,即,给出一阶逻辑公式与概念和术语公理集等价的充分必要条件.

文献^[14]中关于(包含构造子:原子概念、顶概念、概念交、完全存在约束)概念和术语公理集表达能力的刻画,是我们工作的起点.在中增加概念并构造子,得到的描述逻辑称为.文中给出了的模拟关系,

建立了其概念和术语公理集的表达能力的刻画定理.本文有以下3点贡献:

· 给出了描述逻辑的模拟关系,将概念的表达能力刻画定理扩充到的情形(定理5);

· 建立了的布尔型术语公理集(允许否定、蕴含等布尔联结词作用于术语公理所形成的TBox)的表达能力刻画定理(定理7);

· 将术语公理集的表达能力刻画定理扩充到的情形(定理8).

本文第1节是预备知识,主要包括以下内容:描述逻辑的语法和语义介绍;描述逻辑概念及术语公理集到一阶逻辑的翻译;解释之间的互模拟关系及其性质,表达能力与互模拟之间的联系.第2节给出的模拟关系,建立概念的表达能力刻画定理.即给出一阶逻辑公式与的概念等价的充分必要条件.第3节将的模拟关系提升为全局模拟关系,建立的布尔型术语公理集及术语公理集的表达能力刻画定理.即给出一阶逻辑公式与术语公理集等价的充分必要条件.第5节是相关工作.第6节是总结及工作展望.

1 预备知识

本节是文中的预备知识.第1.1节主要介绍描述逻辑的语法和语义.第1.2节给出描述逻辑到一阶逻辑的翻译.第1.3节给出描述逻辑解释之间的互模拟关系及表达能力与互模拟两者之间的联系.

1.1 描述逻辑

描述逻辑的基本符号包括:

(1) 由概念名组成的可数集N_C;

(2) 由角色名组成的可数集合N_R;

(3) 由个体名组成的可数集合N_I.

从这些基本符号出发,可以构造出的概念.

定义1. 中的概念由如下产生式生成:

其中,AÎN_C,rÎN_R,C,D表示的两个概念.

的一个TBox T是有穷条形如CD的概念包含式的集合,其中,C,D分别是的任意两个概念.CºD可以表示为相应的两个概念包含式CD,DC.

下面给出的语义定义.

定义2. 描述逻辑的一个解释I是一个二元组(D^I,×^I),其中,非空集合D^I表示论域,×^I是一个解释函数,使得对任意的概念名A,A^IÍD^I;对任意的角色名r,r^IÍD^IxD^I;并且对任意个体名a,a^IÎD^I.

依据概念名和角色名的解释,我们可以递归地给出一个的概念C的解释.

定义3. 任意给定一个的概念C,概念C的解释递归定义如下:

· T^I=D^I;

· (CóD)^I=C^IÇD^I;

· (CD)^I=C^IÈD^I;

· ($r.C)^I={xÎD^I|存在yÎD^I满足(x,y)Îr^I并且yÎC^I}.

一个解释I满足一个概念包含式CD,如果C^IÍD^I,记作ICD.一个解释I是一个TBox T的模型,如果对任意的CDÎT,都有ICD,记作IT.

1.2到一阶逻辑的翻译

正如本文开始部分所提到的,一个逻辑的表达能力可以有多种不同的角度刻画,文中考虑的是描述逻辑的相对表达能力.即构建描述逻辑到一阶逻辑的翻译,利用解释之间的互模拟关系,建立一阶逻辑公式与概念和术语公理集等价的充分必要条件,从而给出描述逻辑表达能力的刻画.

描述逻辑到一阶逻辑的翻译是将原子概念名对应到一阶逻辑的一元谓词符号,原子角色名对应到二元谓词符号,将每一个概念翻译为一阶逻辑的开公式.描述逻辑到一阶逻辑的翻译s形式定义如下:

· "=(x=x),"=(y=y);

·

·

· (CóD)=,(CóD)=

· (CD)=,(CD)=

·

由概念的翻译,可以得到的TBox T的翻译,即

在语义翻译方面,描述逻辑的解释可以直接对应为一阶逻辑的解释.因此,在文中我们将不对描述逻辑的解释和一阶逻辑的解释做特别的区分.由上述翻译可以看出:描述逻辑的一个概念翻译为一阶逻辑的一个开公式,而术语公理集翻译为一阶逻辑的一个闭公式.

一阶逻辑的开公式a(x)在一个解释I下可满足,记作Ia(x)[x/d].这里,符号[x/d]表示将论域中的元素d指派给自由变元x.上述翻译s是保持公式和TBox T的可满足性.

命题1. 对任意的概念C和解释I,dÎC^I,当且仅当I[x/d].

命题2. 对任意的TBox T和解释I,IT,当且仅当I

注意:并不是所有的描述逻辑都能翻译到一阶逻辑的子部分.例如,带传递闭包构造子的描述逻辑,就需要在一阶逻辑的语言中增加无穷并(infinitary disjunction)加以表达.

1.3 互模拟关系

互模拟是论域上的一类具有特殊性质的二元关系,其在刻画系统之间的并发和通信方面起着重要的作用.下面分别给出描述逻辑解释之间互模拟的定义^[15]以及其相应的性质.

定义4^[15]. 任意给定两个描述逻辑的解释和一个上的二元关系Z称为I₁到I₂的一个互模拟(记作Z:I₁ÇI₂),如果下面3个条件成立:

· 对任意的如果d₁Zd₂,那么对任意的概念名A,都有当且仅当

· 对任意的角色名r,如果d₁Zd₂,(d₁,e₁)Î那么存在e₂Î使得(d₂,e₂)Î并且e₁Ze₂;

· 对任意的角色名r,如果d₁Zd₂,(d₂,e₂)Î那么存在e₁Î使得(d₁,e₁)Î并且e₁Ze₂.

命题3. 令I₁和I₂分别是描述逻辑的两个解释,那么:

(1) 令Z={(x,x)|xÎ那么Z是I₁到I₁的互模拟;

(2) 令Z₁,Z₂分别是I₁到I₂以及I₂到I₃的互模拟,那么Z₁ÑZ₂={(d,d²)|存在d¢,使得dZ₁d¢,d¢Z₂d²}是一个互

模拟关系;

(3) 如果Z是I₁到I₂互模拟关系,那么Z的逆关系Z^-1是I₂到I₁的互模拟关系;

(4) 如果Z是I₁到I₂互模拟关系的集合,那么也是I₁到I₂的互模拟关系.

证明:由互模拟的定义直接验证.

互模拟关系是分析逻辑表达能力的一个强有力的工具,下面给出表达能力与互模拟关系两者之间的联系.

定义5^[15]. 令a(x)是一阶逻辑的一个开公式.称a(x)在互模拟关系下是被保持的,如果对任意的解释I₁和I₂,

任意的以及I₁到I₂所有的互模拟关系Z,若d₁Zd₂,则有:如果I₁a(x)[x/d₁],那么I₂a(x)[x/d₂].

在描述逻辑ALC中,概念的表达能力有如下类似van Benthem刻画定理的结论:

定理4^[15]. 令a(x)是一阶逻辑的一个开公式,a(x)等价于描述逻辑ALC的某个概念C,当且仅当该公式在互

模拟关系下是被保持的.

定理4精确地刻画了一阶逻辑的开公式与ALC中的概念C等价的充分必要条件.但是,定理4的结果并不在所有的描述逻辑中成立,例如,在ALC中增加绝对数量限制构造子,那么定理4的结果在ALCN中不成立.

令C=≥2.r,其中,

·

·

令Z={(a,a¢),(b,b¢),(b,c¢),(c,c¢)},可以验证,Z是一个互模拟关系.但是,

2中概念的表达能力刻画

作为中TBox的表达能力刻画基础,先讨论中概念的表达能力.首先给出的模拟关系,然后给出的表达能力刻画定理及相应的推论.

定义6. 令分别是描述逻辑的两个解释.一个的模拟Z是上的一个非

空二元关系,并且满足如下条件:

(1) 如果d₁Zd₂,那么对任意的原子概念名A,如果

(2) 对任意的角色名r,如果(d₁,e₁)Î,d₁Zd₂,那么存在e₂Î使得(d₂,e₂)Î并且e₁Ze₂.

对比ALC的互模拟关系,的模拟关系有如下两个特点:

· 由于缺少概念否定构造子,所以模拟关系中的条件(1)只取1个方向的结果成立;

· 模拟关系的条件(2)对应完全存在约束构造子.

当Z是连接d₁和d₂的模拟时,记作Z:(I₁,d₁)¶(I₂,d₂).这里需要指出的是,Lutz等人在文献^[14]中定义的模拟关系,其实质上是模拟关系.由此,在刻画的概念和术语公理集表达能力时,就不需要对一阶逻辑的公式增加额外的约束.

一阶逻辑的一个公式a(x)在模拟下是被保持的,当且仅当对任意的解释I₁和I₂,任意的以及I₁到I₂所有的模拟Z,都有:如果d₁Zd₂并且I₁a(x)[x/d₁],那么I₂a(x)[x/d₂].

依据上述模拟关系的定义,有如下中概念表达能力的刻画定理:

定理5. 令a(x)是一阶逻辑的一个开公式.a(x)等价于描述逻辑的某个概念C,当且仅当该公式在模拟下是被保持的.

证明思路:如果a(x)等价于描述逻辑的某个概念C,则可对概念C的结构做归纳,证明a(x)在的模拟下是被保持的.假设a(x)在模拟下是被保持的,令con(a(x))是满足如下条件的集合:对任意的bÎ con(a(x)),都有a(x)b,并且存在的概念C,使得如果能证明con(a(x))a(x),那么由一阶逻辑的紧致性定理,就有定理5的结论成立.假设con(a(x))a(x),那么存在一个解释I,使得Icon(a(x))[x/w],但是I a(x)[x/w].

令G={|C是的概念并且wÏC^I}.如果证明{a(x)}ÈG是可满足的,那么存在一个解释J,使得Ja(x)[x/v],JG[x/v].我们的目标是构造一个解释J到解释I的一个模拟关系Z,使得Z:(J,v)¶(I,w).因为a(x)在模拟下是被保持的,所以Ia(x)[x/w],这与Ia(x)[x/w]矛盾.在构建的模拟关系时,我们还需要解释I扩充为w饱和模型才能达到上述目的.令I^*是I的w饱和模型.定义Z是上的一个二元关系,满足如下条件:d₁Zd₂,当且仅当对的任意概念D,如果d₁ÎD^J,则d₂Î上述Z是一个模拟.又因为I^*是I的w饱和模型,所以对任意的的概念D,wÎD^I,当且仅当wÎ由此,可以完成定理的证明.具体的证明

细节参见附录1.

定理5的结论是文献^[14]定理5的推广.即,将描述逻辑中的概念表达能力的刻画结果推广到了的情形.假定S是比包含更多构造子的描述逻辑系统,由定理5的结论,有如下的推论:

推论6. 令S是比包含更多构造子的描述逻辑系统.对于S的任意概念C,下面两个条件是等价的:

(1) 存在的概念与等价C;

(2) C对应的一阶公式在模拟下被保持.

由推论6可知:S中的一个概念C能否用的一个等价概念重写(concept rewriting),当且仅当概念C所对应的一阶公式在模拟下被保持.更进一步地,如果C不能被的一个等价概念重写,那么能否找到的一个概念D,使得CD,并且D的长度是最短的.这个问题就是概念C的最佳逼近问题(best approximation problem),具体内容详见文献^{[16, 17]}.

3中TBox的表达能力刻画

下面第3.1节给出全局模拟关系及布尔型TBox的表达能力刻画定理;第3.2节介绍描述逻辑一簇解释不相交并的定义,并给出中TBox的表达能力刻画定理.

3.1 布尔型TBox的表达能力刻画

中TBox的表达能力刻画,是建立在其概念表达能力刻画的基础上的.由描述逻辑到一阶逻辑的翻译可以看出:的概念翻译为一阶逻辑的包含一个自由变元的开公式,而TBox T翻译为一阶逻辑的闭公式.由此,一个自然的想法是将模拟关系从“局部”提升为“全局”模拟关系.

定义7. 任意给定描述逻辑的两个解释I₁和I₂,一个I₁至I₂的全局模拟关系(记作I₁;I₂),如果下面两个条件成立:

(1) 对任意的d₁Î都存在d₂Î使得Z₁:(I₁,d₁)¶(I₂,d₂)并且Z₂:(I₂,d₂)¶(I₁,d₁);

(2) 对任意的d₂Î都存在d₁Î使得Z₂:(I₂,d₂)¶(I₁,d₁)并且Z₁:(I₁,d₁)¶(I₂,d₂).

一阶逻辑的一个闭公式a在全局模拟关系下是不变的,当且仅当对任意的两个解释I₁和I₂以及I₁至I₂所有的全局模拟关系,如果I₁;I₂,那么I₁a,当且仅当I₂a.直觉上,我们应该证明:一阶逻辑的闭公式a等价于的某个TBox T,当且仅当该公式在全局模拟下不变的.但正如文献^[14]所指出的,上述刻画所得到的将是中的布尔型的Tbox.这里,布尔型TBox是指术语公理集中允许出现形如:Ø(CD),(CD)® (EF),(CD)Ú(EF),(CD)Ù(EF)等表达式作为术语公理.

定理7. 令a是一阶逻辑的一个闭公式.a等价于中的某个布尔型TBox T,当且仅当该公式在全局模拟下不变.

证明思路:假设a等价于中的某个布尔型TBox T.对TBox的结构,即,分T={CD},{Ø(CD)}或者{(CD)®(EF)}这3种情况讨论,可以证明a在全局模拟下不变.假设a在全局模拟下不变,并且令con(a)是满足如下条件的集合:对任意的bÎcon(a),都有ab并且存在的布尔型TBox T,使得T^s=b.如果能够证明con(a)a,那么由一阶逻辑的紧致性定理,可得与a等价的TBox T.假设con(a)a.我们的目标是构造2个w饱和模型I,J,使得IØa,Ja并且I; J.由a在全局模拟下不变,即可导出Ia,IØa的矛盾.

令I是con(a)È{Øa}的模型:

G={j|Ij,j=(CD₁…D_n)^s或者j=Ø(CD₁…D_n)^s,这里的C,D₁,D₂,…,D_n为概念}.

用反证法,可以证明{a}ÈG是可满足的.令J是{a}ÈG的模型.由模型论的知识,对任意一个一阶逻辑的解释(在可数语言下)I,总存在一个w饱和模型I^*,使得对任意的一阶逻辑的公式j,Ij,当且仅当I^*j.因此,不失一般性,假定I,J均是w饱和模型.证明I; J,还需要证明如下两点事实:

(1) 对任意的dÎD^I,存在eÎD^J,使得对任意的概念C,dÎC^I,当且仅当eÎC^J;

(2) 对任意的eÎD^J,存在dÎD^I,使得对任意的概念C,eÎC^J,当且仅当dÎC^I.

令Z₁是D^IxD^J上的一个二元关系,满足如下条件:dZ₁e,当且仅当对的任意概念C,如果dÎC^I,则eÎC^J;令Z₂是D^JxD^I上的一个二元关系,满足如下条件:dZ₂e,当且仅当对的任意概念C,如果eÎC^J,则dÎC^I.由I,J均是w饱和模型及上述2点事实,可以证明I; J.于是就有定理7成立.具体的证明细节参见附录2.

3.2TBox的表达能力刻画

为了能够刻画TBox而不是布尔型TBox,文献^[14]中运用解释的不相交并来解决上述问题.令(I_i)_iÎI是一簇描述逻辑的解释.(I_i)_iÎI的不相交并J定义如下:

· 其中,i¹j;

· AÎN_C;

· rÎN_R.

一个一阶逻辑的闭公式a在不相交并下是不变的,当且仅当对所有不相交的解释(I_i)_iÎI,I_ia,iÎI,当且仅当不相交的并Ja.布尔型的TBox在不相交的并下不是不变的.以下是文献^[14]中的例子:

例1:令T₁={("A)Ú("B)},,则I₁和I₂的不相交的并I为

显然,I₁和I₂满足T₁,但是IT₁.令T₂={Ø("A)},显然,IT₂,但是I₁T₂.

定理8. 令a是一阶逻辑的一个闭公式.a等价于中的某个TBox T,当且仅当该公式在全局模拟和不相交的并下不变.

证明思路:假设a等价于中的某个TBox T.不失一般性,假设T={CD},容易验证a在全局模拟和不相交的并下不变.假设a在全局模拟和不相交的并下不变,并且令con(a)={(CD)^s|a(CD)^s}.如果能够证明con(a)a,那么由一阶逻辑的紧致性定理就有:存在一个TBox T与a等价.假设con(a)a,则con(a)È{Øa}可满足.我们的目标是构造两个w饱和模型I,J,使得IØa,Ja,并且I; J.由a在全局模拟下不变,即可导出Ia,IØa的矛盾.对每一个形如(CD₁…D_n)^sÏcon(a),记I_CD1…Dn是con(a)的一个模型,并且满足条件:I_CD1…Dn(CD₁…D_n).令I是所有I_CD1…Dn及con(a)È{Øa}的一个模型不相交的并,则I(CD₁…D_n),IØa.接下来,对每一个形如(CD₁…D_n)^sÏcon(a),记J_CD1…Dn是a的一个模型,并且满足条件:J_CD1…DnCD₁…D_n.令J是所有J_CD1…Dn不相交的并,则JCD₁…D_n,Ja.类似于定理7的证明思路,证明I; J,于是就有定理8成立.具体的证明细节参见附录3.

定理8的结论是文献^[14]定理17的推广.即,将描述逻辑中的TBox表达能力的刻画结果推广到了的情形.假定S是比包含更多构造子的描述逻辑系统,由定理8的结论,有如下推论:

推论9. 令S是比包含更多构造子的描述逻辑系统.对S的任意TBox T,下面两个条件是等价的:

(1) 存在中的TBox T'与T等价;

(2) T所对应的一阶公式在全局模拟和不相交的并下不变.

推论9表明:S中的TBox T能否用中的一个等价TBox T'重写,当且仅当T在全局模拟关系和不相交的并下不变.在文献^{[18, 19]}中,一个TBox被看作是一个本体,那么在这个意义下,推论9刻画了在怎样的条件下,S中的本体与中的本体表达能力是相同的.

4 相关工作

Baader^[20]较早地研究了描述逻辑表达能力、形式化地给出了描述逻辑术语公理集表达能力的定义,其工作主要侧重分析描述逻辑不同术语公理集之间表达能力的差异;而对描述逻辑的概念和术语公理集,则没有建立相应的表达能力刻画定理.

Borgida^[21]分析不同描述逻辑与哪些一阶逻辑的子部分表达能力等价问题,其工作主要侧重于分析不同描述逻辑概念与一阶逻辑子部分的公式在语法层次上的相互等价转换问题;而对描述逻辑的概念和术语公理集,也没有给出相应的表达能力刻画定理.

Kurtonina等人^[15]以描述逻辑FL_-为出发点,给出了FL族的含不同构造子的描述逻辑的模拟关系,建立了FL族的概念表达能力的刻画定理以及FL族表达能力划分结果,但是没有给出FL族术语公理集表达能力刻画定理.

Lutz等人^[14]给出了包含较多构造子的描述逻辑ALCQIO和两个包含构造子较少的描述逻辑,以及DL-Lite的概念和术语公理集的表达能力刻画定理.本文的工作是对Lutz等人工作的扩展.

5 总结及工作展望

表达能力和推理复杂性是一个逻辑的两个重要特征,也是一对相互制约的关系.本文给出了的模拟关系,并建立了中概念和术语公理集的表达能力刻画定理.上述结果为寻求表达能力与推理复杂性之间的最佳平衡提供了有效的支持.后续工作包括以下3点:

· 本文是将中概念和术语公理集的表达能力结果推广到增加并构造子的的描述逻辑系统.下一步可以考虑增加原子概念否定构造子或角色构造子等其他构造子的情形下,描述逻辑系统概念和术语公理集的表达能力问题.

· 推论6和推论9仅仅是给出了用中的概念和术语公理集重写其他描述逻辑系统的概念和术语公理集的初步结果,更进一步地,上述问题的可计算性以及其计算的复杂性值得做更深入的研究.

· 在表达能力刻画定理的证明中,主要使用了一阶逻辑的紧致性定理,但不是所有的描述逻辑都能翻译到一阶逻辑上.比如,包含带传递闭包构造子的描述逻辑就需要在一阶逻辑的语言中增加无穷并加以表达,而包含无穷并的一阶逻辑不具有紧性^[22].因此,为刻画上述描述逻辑系统的表达能力,需要给出新的方法.

附录:表达能力刻画定理的证明

在给出完整证明之前,首先介绍在证明中需要用到的两个重要结论:

(1) 令I是一阶逻辑语言L的解释,我们称I是一个w饱和模型,如果S是语言L¢下的公式的集合,其中,L¢是L通过增加有穷多个新的个体符号所得的,并且每个S的有穷子集在I的L¢-膨胀模型下可满足,那么S也在I的L¢-膨胀模型下可满足;

(2) 对任意一个一阶逻辑的解释(在可数语言下)I,总存在一个饱和w模型I^*,使得对任意的一阶逻辑的公式j,Ij,当且仅当I^*j.

上述两个结论,在模型论的书籍中均可查到,更多有关模型论方面的知识可以参见文献^[23].

附录1:概念表达能力刻画定理的证明

定理5. 令a(x)是一阶逻辑的一个开公式.a(x)等价于描述逻辑的某个概念C,当且仅当该公式在模拟下是被保持的.

证明:Þ施归纳于概念C的结构.

· 情形1:C为原子概念名.

由定义6的条件(1)可得,a(x)在模拟下是被保持的.

· 情形2:C=AóB.

假设d₁Zd₂,d₁Î(AóB)于是有由归纳假设即d₂Î(AóB)

· 情形3:C=AB.

假设d₁Zd₂,d₁Î(AB)于是有或者由归纳假设或者即d₂Î(AB)

· 情形4:C=$r.D.

假设d₁Zd₂,因为所以存在e₁Î使得(d₁,e₁)Î并且e₁Î由的模拟定义的条件(2),存在e₂Î使得(d₂,e₂)Î并且e₁Ze₂.由归纳假设,e₂Î即

Ü假设a(x)在模拟下是被保持的,并且令con(a(x))是满足如下条件的集合:对任意的bÎcon(a(x)),都有a(x)b,并且存在的概念C,使得先证明如下引理:

引理1. 如果con(a(x))a(x),那么存在的某个概念C,使得a(x)与C等价.

证明:因为con(a(x))a(x),所以由一阶逻辑的紧致性定理,就有b₁,…,b_nÎcon(a(x)),并且b₁Ù…Ùb_na(x).令C=C₁ó…óC_n,其中,则a(x)与C等价.

下面证明con(a(x))a(x).假设con(a(x))a(x),那么存在解释I,使得Icon(a(x))[x/w],但是Ia(x)[x/w].令G={|C是的概念并且wÏC^I}.

引理2. {a(x)}ÈG是可满足的.

证明:假设{a(x)}ÈG是不可满足的,那么存在ÎG,使得a(x)即

a(x)

又因为Icon(a(x))[x/w],所以I()[x/w].由命题1,wÎ(C₁…C_n)^I.于是存在某个i,1≤i≤n,使得.这与G的构造矛盾.

引理3. 令J是满足{a(x)}ÈG的模型.即,Ja(x)[x/v],并且JG[x/v].对任意的的概念D,如果vÎD^J,那么,wÎD^I.

证明:假设wÏD^I,那么ÎG.于是J[x/v].即J[x/v],也就是说,vÏD^J.

令I^*是I的w饱和模型.令Z是上的一个二元关系,满足如下条件:d₁Zd₂,当且仅当对的任意概念D,如果d₁ÎD^J,则d₂Î下面证明Z是一个模拟.

引理4. Z是一个模拟.

证明:定义6的第1个条件是显然成立的.下面验证条件(2).对任意的角色名r,假设(d₁,e₁)Îr^J,d₁Zd₂.

令S={D|D是概念并且e₁ÎD^J}.对任意的D₁,¼,D_nÎS,就有e₁Î(D₁ó…óD_n)^J.因为(d₁,e₁)Îr^J,所以d₁Î$r.(D₁ó…óD_n)^J.由d₁Zd₂,有d₂Î$r.(D₁ó…óD_n)即,存在e₂Î使得(d₂,e₂)Î并且e₂Î(D₁ó…óD_n)即,e₁Ze₂.由此,我们已经证明S的任意有穷子集都在I^*下可满足,而I^*又是w饱和模型,于是,S在I^*下可满足.即,如果(d₁,e₁)Îr^J,d₁Zd₂,那么存在e₂Î使得(d₂,e₂)Î并且e₁Ze₂.

最后,因为I^*是I的w饱和模型,所以对任意的的概念D,wÎD^I,当且仅当wÎ由引理3和引理4,存在的模拟,使得vÎD^I与wÎ具有Z关系.又因为a(x)是在模拟下被保持的,所以由Ja(x)[x/v],有Ia(x)[x/w].这与Ia(x)[x/w]矛盾.于是,con(a(x))a(x)结论成立.再由引理1可知,定理5成立. 

附录2:布尔型TBox表达能力刻画定理的证明

定理7. a是一阶逻辑的一个闭公式.a等价于中的某个布尔型TBox T,当且仅当该公式在全局模拟下不变.

证明:Þ下面分3种情况讨论:

· 情形1:T={CD}.

令I₁和I₂是任意两个解释,并且I₁; I₂.假设I₁a.因为T^s与a等价,所以I₁T^s.即,I₁下面证明I₂a.假设对任意的d₂Î都有I₂[x/d₂].因为I₁; I₂,所以存在d₁Î,使得I₁[x/d₁],于是就有I₁[x/d₁].又因为(I₁,d₁)¶(I₂,d₂),所以I₂[x/d₂],即I₂.类似地可以证明:如果I₂a,那么I₁a.

· 情形2:T={Ø(CD)}.

假设I₁a.因为T^s与a等价,所以I₁.即,I₁.

由归纳假设就有:I₂.即I₂.类似地可以证明:如果I₂a,那么I₁a.

· 情形3:T={(CD)®(EF)}.

假设I₁a.因为T^s与a等价,所以I₁.即:如果I₁,那么I₁.由归纳假设就有:如果I₂,那么I₂.即,I₂a.类似地可以证明:如果I₂a,那么I₁a.

由上述3种情形可得:如果a等价于中的某个布尔型TBox T,那么a在全局模拟下不变.

Ü假设a在全局模拟下不变,并且令con(a)是满足如下条件的集合:对任意的bÎcon(a),都有ab,并且存在的布尔型TBox T,使得T^s=b.先证明如下引理:

引理5. 如果con(a)a,那么存在中的布尔型TBox T,使得a与T等价.

证明:因为con(a)a,所以由一阶逻辑的紧致性定理,就有b₁,¼,b_nÎcon(a),并且b₁Ù…Ùb_na.

令其中则a与T等价.

下面证明con(a)a.假设con(a)a,则con(a)È{Øa}可满足.令I是con(a)È{Øa}的模型,G={j|Ij, j=(CD₁…D_n)^s,或者j=Ø(CD₁…D_n)^s,这里,C,D₁,¼,D_n为的概念}.

引理6. {a}ÈG是可满足的.

证明:假设{a}ÈG是不可满足的,那么存在j₁,¼,j_nÎG,使得aØ(j₁Ù…Ùj_n).即aØj₁Ú…ÚØj_n.

又因为Icon(a),所以存在某个i,1≤i≤n,使得IØj_i.这与G的构造矛盾.

令J是{a}ÈG的模型.由模型论的知识,对任意一个一阶逻辑的解释(在可数语言下)I,总存在一个w饱和模型I^*,使得对任意的一阶逻辑的公式j,Ij,当且仅当I^*j.因此不失一般性,假定I,J均是w饱和模型.

如果I; J,那么由a在全局模拟下不变,便有Ia,Ja.这与I是con(a)È{Øa}的模型矛盾.即,假设con(a)a错误.由引理5,于是有定理7成立.下面证明I; J.

引理7. 对任意的dÎD^I,存在eÎD^J,使得对任意的概念C,dÎC^I,当且仅当eÎC^J.

证明:对任意的dÎD^I,令S⁺={C|dÎC^I,C为概念},S^-={C|dÏC^I,C为概念}.

对任意的因为dÎ(ó…ó)^I,但是dÏ(…)^I,所以,

Ió…óó…ó

又因为I,J满足相同形如CD₁…D_n术语公理,所以Jó…óó…ó即

J

于是有:存在e¢ÎD^J,使得e¢Î(ó…ó)^J,但是e¢Ï(…)^J.由J是饱和模型,所以对任意的dÎD^I,存在eÎD^J,使得对任意的CÎS⁺,若dÎC^I,则eÎC^J和任意的CÎS^-;若dÏC^I,则eÏC^J.即,dÎC^I,当且仅当eÎC^J成立. 引理7成立.

引理8. 对任意的eÎD^J,存在dÎD^I,使得对任意的概念C,eÎC^J,当且仅当dÎC^I.

证明:与引理7的证明类似.

令Z₁是D^IxD^J上的一个二元关系,满足如下条件:dZ₁e,当且仅当的任意概念C,如果dÎC^I,则eÎC^J;

令Z₂是D^JxD^I上的一个二元关系,满足如下条件:eZ₂d,当且仅当对的任意概念C,如果eÎC^J,则dÎC^I.

类似引理4,可以证明Z₁,Z₂是两个模拟关系.再由引理7和引理8,就有I; J,从而定理7成立.

附录3:TBox表达能力刻画定理的证明

定理8. 令是a一阶逻辑的一个闭公式.a等价于中的某个TBox T,当且仅当该公式在全局模拟和不相交的并下不变.

证明:Þ不失一般性,假设T={CD}.由定理7情形1的证明可知,a在全局模拟下不变.令(I_i)_iÎI是一簇描述逻辑的解释,I是其不交的并.如果对所有的iÎI,I_iCD,那么由I的构造,就有ICD;反之,如果ICD,那么由,有:对所有的iÎI,即I_iCD,iÎI.

Ü假设a在全局模拟和不相交的并下不变,并且令con(a)={(CD)^s|a(CD)^s}.如果能够证明con(a)a,那么由一阶逻辑的紧致性定理有:存在一个TBox T与a等价.

假设con(a)a,则con(a)È{Øa}可满足.对每一个形如(CD₁…D_n)^sÏcon(a),记I_CD1…Dn是con(a)的一个模型,并且满足条件:I_CD1…DnCD₁…D_n.令I是所有I_CD1…Dn及con(a)È{Øa}的一个模型不相交的并,则ICD₁…D_n,IØa.

接下来,对每一个形如(CD₁…D_n)^sÏcon(a),I_CD1…Dn是a的一个模型,并且满足条件:

I_CD1…DnCD₁…D_n.

令J是所有I_CD1…Dn不相交的并,则JCD₁…D_n,Ja.

如果I; J,那么由a在全局模拟下不变,于是有Ia,Ja.这与IØa矛盾.即,假设con(a)a错误,于是有定理8成立.下面证明I; J.

引理9. 对任意的dÎD^I,存在eÎD^J,使得对任意的概念C,dÎC^I,当且仅当eÎC^J.

证明:与引理7的证明类似.

引理10. 对任意的eÎD^J,存在dÎD^I,使得对任意的概念C,eÎC^J,当且仅当dÎD^I.

令Z₁是D^IxD^J上的一个二元关系,满足如下条件:dZ₁e,当且仅当对的任意概念C,如果dÎD^I,则eÎD^J;

令Z₂是D^JxD^I上的一个二元关系,满足如下条件:eZ₂d,当且仅当对的任意概念C,如果eÎD^J,则dÎC^I.

类似于引理4,可以证明Z₁,Z₂是两个模拟关系.再由引理9和引理10,有I; J,从而定理8 成立.