软件学报  2014, Vol. 25 Issue (1): 64-77   PDF    
基于OBDD的描述逻辑εL循环术语集推理
古天龙, 吕思菁, 常 亮, 徐周波    
(广西可信软件重点实验室(桂林电子科技大学),广西 桂林 541004)
摘要:循环术语集推理是描述逻辑研究中面临的难点问题,尚未得到很好的解决.有序二叉决策图(ordered binary decision diagram,简称OBDD)是一种对布尔函数进行紧凑表示和高效操作的数据结构,适用于表示和处理大规模问题.将OBDD应用于描述逻辑循环术语集的推理.首先,针对描述逻辑εL中的循环术语集,给出了描述图上关于最大模拟关系的重要性质,并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上,应用布尔函数对描述图进行编码,给出了基于OBDD求解最大模拟关系的方法,进而给出了最大不动点语义下基于OBDD对概念包含关系进行判定的算法;接下来,基于OBDD给出了求解描述图中可以到达循环路径的所有结点的方法,进而给出了最小不动点语义下基于OBDD对概念包含关系进行判定的算法;最后,对算法的正确性、复杂度等进行了分析和证明,并对算法进行了编程实现,给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径,也为OBDD在逻辑推理中的应用提供了新的案例.
关键词描述逻辑εL     循环术语集     有序二叉决策图     概念包含关系     不动点语义    
OBDD-Based Reasoning for Terminological Cycles of the Description Logic εL
GU Tian-Long, LÜ Si-Jing, CHANG Liang, XU Zhou-Bo    
(Guangxi Key Laboratory of Trusted Software (Guilin University of Electronic Technology), Guilin 541004, China)
Abstract:Reasoning about terminological cycles of description logics is a hard problem that needs to be solved. Ordered binary decision diagram (OBDD) is a data structure suitable for dealing with large-scale problems since through the diagram Boolean functions can be represented compactly and computed efficiently. In this paper, OBDD is adopted to reason about terminological cycles of description logics. First, for terminological cycles of the description logic εL, with the help of set representation and operation, a property about the greatest simulation relationship on description graphs of terminological cycles is specified and proved. Second, by encoding description graphs of terminological cycles as Boolean functions, an OBDD-based procedure for computing the greatest simulation relationship is proposed, and based on this procedure an algorithm is presented for deciding the subsumption relationship between concepts under the greatest fix-point semantics. Third, based on OBDD, a procedure for calculating all the nodes which can reach cycle paths in a description graph is proposed, and based on this procedure an algorithm for deciding the subsumption relationship under the least fix-point semantics is also presented. Finally, the correctness and time complexity of both algorithms are proved; the computing performance of both algorithms are also demonstrated by a set of experiments. This work provides an effective approach for reasoning about terminological cycles of description logics; it also provides a new case for applying OBDD in the fields of logical reasoning.
Key words: description logic εL     terminological cycles     ordered binary decision diagram     concept subsumption     fix-point semantics    

作为一类用于知识表示的形式化工具,描述逻辑在信息系统、软件工程、自然语言处理等领域得到了成功应用,尤其是在语义Web中扮演着关键角色,成为了语义Web本体语言OWL的逻辑基础.描述逻辑的主要特点在于提供了命题逻辑所无法比拟的刻画能力,同时保证了相关推理问题的可判定性,此外还拥有高效的推理机制作为支撑[1].

循环术语集是描述逻辑长期以来的研究难点,其语义定义问题和推理算法问题尚未得到很好的解决.因此,在目前对描述逻辑的研究和应用中,一般都假设所考察的知识库中不含有循环定义.但实际上,循环定义不仅可以扩充描述逻辑的表达能力,而且在许多应用中是不可避免的[2, 3].此外,循环定义还能够方便用户建立描述逻辑知识库,使所刻画的知识符合人们的直觉;如果不使用循环定义,则会使得最终建立的知识库非常复杂,用户也难以理解[4, 5].例如,在考察一个有向图时,令Node和edge分别对应于图中的所有结点和有向边,则我们可以将图中出现在无限长的通路上的所有结点刻画为[6]:Inode≡NodeΠ彐edge.Inode;由于Inode出现在自身的定义式中,从而形成了循环定义.通常也将含有循环定义的知识库称为循环术语集[6].

Nebel[4, 5]最早对循环术语集进行了研究,提出了循环术语集的3种语义:描述语义、最大不动点语义和最小不动点语义.其中,描述语义与一般情况下(即不含有循环定义时)描述逻辑中采用的语义相同;但是,由于循环定义的出现,使得一个循环术语集可能具有多个基于描述语义的解释.最大不动点语义和最小不动点语义以定义在解释结构上的偏序关系为基础,分别将基于该偏序关系的最大不动点和最小不动点作为唯一的语义解释.在多数情况下,采用最大不动点语义或最小不动点语义能够更好地符合人们刻画知识库的初衷.

在Nebel给出的语义解释的基础上,许多研究者对循环术语集的推理问题进行了研究.其中,针对由描述逻辑FL0刻画的循环术语集,Baader[2]借助有穷状态自动机给出了对概念的可满足性和概念之间包含关系进行判定的算法.针对由描述逻辑ελ刻画的循环术语集,Baader[6]借助描述图给出了对概念的可满足性和概念之间包含关系进行判定的算法.之后,蒋运承等人[7]将Baader的工作扩展到描述逻辑εLN,给出了εLN循环术语集在不动点语义下关于概念可满足性和概念包含关系的推理算法.王驹等人[8]借助描述图和模拟关系,给出了描述逻辑vλ循环术语集关于可满足性和概念包含关系的推理算法.但到目前为止,研究者尚未对这些算法加以实现.目前,著名的描述逻辑推理机也不能在不动点语义下对描述逻辑循环术语集进行推理.

有序二叉决策图(ordered binary decision diagram,简称OBDD)[9]是一种对布尔函数进行紧凑表示和高效操作的数据结构.由于其可以有效地缓解乃至避免对布尔函数进行处理时可能出现的状态组合爆炸问题,因而在硬件电路综合与验证、组合优化、智能调度、模型检测等领域都得到了成功应用[9, 10].能否在逻辑推理领域发挥出OBDD的优点,是相关研究者关注的问题.许多研究者已在这方面进行了探索,其中,Uribe和Stickel[11]将OBDD应用于命题公式的可满足性判定,显示了OBDD在命题逻辑公式可满足性判定方面具有巨大的应用潜力.Groote[12]将OBDD用于一阶谓词逻辑的推理,将OBDD对命题逻辑的推理提升到一阶谓词逻辑层面. Marrero[13]将OBDD运用于分支时态逻辑CTL的推理,给出了基于OBDD的CTL可满足性判定算法.Pan等人[14]将OBDD应用于模态逻辑的可满足性判定,实验结果表明,该方法在逻辑公式中出现模态词较多时具有明显的性能优势.

针对描述逻辑,Keller[15]最先提出基于OBDD进行逻辑推理的思路,但并未给出算法.之后,Rudolph等人[16]针对描述逻辑ALCIb首次给出了基于OBDD的推理算法.由于可以将描述逻辑SHIQ的一致性问题在可满足性等价的情况下转换为描述逻辑ALCIb的一致性问题,因而,Rudolph等人实际上也基于OBDD给出了描述逻辑SHIQ的一致性判定算法[17].但是,Rudolph等人的算法不支持循环术语集;虽然Rudolph等人[16, 17]在论文中没有明确地假设不含有循环定义,但其论文中考察的描述逻辑在语义定义上采用的是描述语义,因而相应的算法不支持循环定义所要求的最大不动点语义和最小不动点语义.此外,Rudolph等人尚未对算法加以实现,不能从实际计算性能的角度对基于OBDD的推理算法进行考察.

本文将OBDD技术引入到对描述逻辑循环术语集的推理之中,针对由描述逻辑εL刻画的循环术语集,在Baader等人[6]给出的基于描述图的判定方法的基础上,本文借助OBDD分别给出最大不动点语义下和最小不动点语义下对概念之间包含关系进行判定的算法.首先,针对最大不动点语义,本文借助集合运算给出描述图上关于最大模拟关系的一个重要性质,并基于该性质给出应用OBDD求解最大模拟关系的方法,进而得到最大不动点语义下应用OBDD判断概念包含关系的算法;其次,针对最小不动点语义,本文借助集合运算给出计算描述图中所有可以到达循环通路的结点的方法.在此基础上,得出最小不动点语义下应用OBDD判断概念包含关系的算法;最后,本文对上述两种算法进行优化实现,给出具体的实验结果.

本文第1节对背景知识进行介绍.第2节和第3节分别给出最大不动点语义下和最小不动点语义下基于OBDD对概念包含关系进行判定的算法.第4节对两种算法的正确性和时间复杂度进行分析,并与描述逻辑推理机Pellet进行实验比较.第5节对相关工作进行考察.第6节总结全文.

1 背景知识

本文涉及的背景知识主要包括3个方面:描述逻辑εL循环术语集,Baader等人给出的关于循环术语集推理的两个定理以及有序二叉决策图.

1.1 描述逻辑εL循环术语集

描述逻辑εL的基本符号包括由角色名组成的集合NR和由概念名组成的集合NC.从这些符号出发可以递归地构造出角色和概念:RεL中的角色当且仅当RNR;令ANC,R为角色,则εL中的概念由如下产生式生成:

εL的解释I=(ΔII)由解释域ΔI和解释函数·I构成.解释函数·I将每个角色名解释为ΔI上的一个关系,将每个概念名解释为ΔI的一个子集,递归定义如下:

(1) 丅I=ΔI;

(2) AIΔI;

(3) RIΔIxΔI;

(4) (CΠD)I=CIDI;

(5) (彐R.C)I={xΔI|彐yΔI使得(x,y)∈RI并且yCI}.

εL的TBox是由形如CD的概念定义式组成的有限集合,其中,CNC,DεL概念.给定一个TBox T,如果概念名C出现在T中概念定义式的左边,则称C;否则,称C为原始概念名.

C是一个被定义的概念名,其概念定义式为CD.如果某个概念名B出现在D中,则称C直接使用了B.将关系“直接使用”的传递闭包称为“使用”.在此基础上,如果TBox中存在某个被定义的概念名在概念定义式中“使用”了自身,则称该TBox中存在循环定义,也称该TBox为循环术语集.

文献中给出了循环术语集的3种语义定义[4, 5].其中,由于描述语义与一般情况下(即不含有循环定义时)描述逻辑中采用的语义相同,本文不再详述.下面引入解释结构上的偏序关系,进而给出εL循环术语集的最大不动点语义和最小不动点语义:

· 首先,给定描述逻辑εL的任一TBox T,令Nrole,Nprim,Ndef是由出现在T中的所有角色名、原始概念名和被定义的概念名组成的集合,并且令Nrole={R1,…,Rn},Nprim={P1,…,Pm}和Ndef={C1,…,Ck};

· 其次,给定一个解释J=(ΔJJ),其中,对于任一RiNrole都有ΔJxΔJ,对于任一PiNprim都有ΔJ.在此基础上,对于任一解释I=(ΔII),如果ΔI=ΔJ,并且对于任一RiNrole和任一PiNprim都有则称解释J是解释I的原始解释.相应地,称解释I是解释J的扩充,或者称I是基于J的解释;

· 最后,给定一个解释J,令集合Int(J):={I|I是基于J的解释},在Int(J)上定义偏序关系≤J如下:I1JI2当且仅当对于任一CiNdef都有CiI1⊆CiI2

显然,由集合Int(J)和偏序关系≤J构成的二元组{Int(J)≤J}是一个完全格.由Tarski不动点定理可知,如果存在单调函数O:Int(J)→Int(J),使得对于任意I1,I2Int(J)来说,当I1J I2时必然有O(I1)≤JO(I2),则函数O必然存在不动点.

给定任一TBox T={C1D1,…,CkDk}和解释J,对函数OT,J:Int(J)→Int(J)定义如下:OT,J(I1)=I2当且仅当对于任一1≤ik都有CiI2≡DiI1容易证明,OT,J是一个单调函数,并且存在最小不动点和最大不动点.

定义1. 令TεL的任一TBox.如果存在某个解释I=(ΔII)使得对于任一概念定义式CDT都有CI=DI,则称IT的一个模型.如果IT的模型,并且存在一个解释J使得IInt(J)而且I是函数OT,J的最大不动点(最小不动点),则称IT的最大不动点模型(最小不动点模型),简称为gfp-模型(lfp-模型).

最大不动点语义仅接受最大不动点模型.相应地,最小不动点语义仅接受最小不动点模型.

定义2. 令TεL的任一TBox,A,BT中被定义的概念,则:

(1) 在最大不动点语义下A包含于B,记为,当且仅当对于T的任一gfp-模型I都有AIBI;

(2) 在最小不动点语义下A包含于B,记为,当且仅当对于T的任一lfp-模型I都有AIBI.

1.2 描述逻辑εL循环术语集的推理定理

为了对循环术语集中的概念包含关系进行判定,Baader等人借助描述图给出了两个定理[6].下面首先引入一些符号和术语,然后对这两个定理进行介绍.本文的算法将建立在这两个定理的基础之上.

给定任一TBox T={C1D1,…,CkDk},称T是正规化的当且仅当对于任一CiDi(1≤ik)来说,Di具有如下形式:

P1Π…ΠPtΠ彐R1.B1Π…Π彐Rs.Bs,

其中,t,s≥0,P1,…,PtNprim,R1,…,RsNrole,B1,…,BsNdef.如果t=s=0,则Di=丅.

给定描述逻辑εL的任一TBox,可以在多项式时间内将其转化为在最大不动点语义(最小不动点语义)下等价的正规化的TBox[6].在本文接下来的内容中,我们假设所讨论的TBox都是正规化的.

定义3. 给定εL的任一TBox T,其描述图是一个三元组GT=(VT,ET,LT),其中,

(1) VT=Ndef,是将T中每个被定义的概念作为一个结点后形成的结点集合;

(2) ETVTxNrolexVT,是用T中的角色名进行标记的有向边的集合;

(3) LT:VT→2Nprim,为每个结点标记T中的若干个原始概念;

(4) LTET满足如下性质:对于任一CVT,如果CT中的概念定义式为CP1Π…ΠPmΠ$R1.B1Π… Π彐Rn.Bn,则有LT(C)={P1,…,Pm}和{(C,R1,B1),…,(C,Rn,Bn)}⊆ET.

例1:考察TBox T={C1P1ΠP2ΠP3Π彐R1.B1Π彐R2.B2Π彐R1.B3,C2P2ΠP3Π彐R2.B2Π彐R1.B3,C3P2ΠP3Π彐R2.B2Π 彐R1.B3,B1≡彐R2.C3,B2≡彐R1.C1,B3P1ΠP2},其描述图如图 1所示.

图 1 例1中TBox T的描述图 Fig. 1 Description graph corresponding to the TBox T in Example 1

定义4. 给定任意两个描述图G1=(V1,E1,λ1)和G2=(V2,E2,λ2),将二元关系ZV1xV2称为G1G2的模拟关系,当且仅当Z满足以下条件:

(1) 如果(v1,v2)∈Z,则有λ1(v1)⊆λ2(v2);

(2) 如果(v1,v2)∈Z,且存在一个结点v'1V1使得(v1,R,v'1)∈ε1,则必存在某个结点v'2V2使得(v2,R,v'2)∈E2和v'1,v'2∈Z

如果ZG1G2的模拟关系,则记为.

借助描述图和模拟关系,可以在最大不动点语义下对概念之间的包含关系进行判定.判定定理如下:

定理1[6]. 给定εL的任一TBox T和其中两个被定义的概念A,B,下面两个命题是互相等价的:

(1)

(2) 对于T的描述图GT,存在GTGT的模拟关系Z,使得(B,A)∈Z.

在最小不动点语义下,也可以借助描述图和模拟关系进行推理.在给出推理定理之前需引入如下概念:

TεL的任一TBox,GT=(Ndef,ET,LT)是T的描述图.对于任意两个结点A,BNdef,如果图GT中存在从AB的一条路径,则记为;如果存在从AB的一条非空路径,则记为.在此基础上,定义CycT如下:CycT:={A|ANdef,并且存在结点BNdef使得

定理2[6]. 令TεL的任一TBox,GT=(Ndef,ET,LT)是T的描述图,G'T是从图GT中删除所有出现在CycT中的结点以及所有与这些结点相连的边之后得到的描述图,则当且仅当满足下列两种情况之一:

(1) ACycT;

(2) ACycT,BCycT,并且存在G'TG'T的模拟关系Z,使得(B,A)∈Z.

以这两个定理为基础,本文将借助OBDD分别给出最大不动点语义下和最小不动点语义下对概念包含关系进行判断的算法.

1.3 有序二叉决策图

有序二叉决策图(OBDD)是一种对布尔函数进行紧凑表示和高效操作的数据结构.给定含有n个命题变元x1,x2,…,xn的任一布尔函数f(x1,x2,…,xn),其OBDD表示是一个十元组W=(N,root,1,0,low,high,Var,π,λ,φ),其中,

(1) N是由结点组成的有限集合;

(2) rootN为根结点;

(3) 0,1∈N为终端结点;

(4) lowhigh是从N\{0,1}到N\{root}的函数,分别为每个非终端结点指定左孩子结点和右孩子结点;

(5) Var={x1,x2,…,xn};

(6) π是对Var中的各个变量指定一种排序,称为变量序;

(7) λ是从N\{0,1}到Var的函数,为每个非终端结点赋予一个变量,并且使得从根结点到终端结点的任一路径上的变量均以变量序p所规定的次序依次出现;

(8) φ为每个结点赋予一个布尔函数,并且满足如下条件:

① 根结点对应的布尔函数为φ(root)=f(x1,x2,…,xn);

② 终端结点对应的布尔函数分别为φ(0)=false和φ(1)=true;

③ 对于每个非终端结点u,其对应的布尔函数为φ(u)=(¬λ(u)∧φ(low(u)))∨(λ(u)∧φ(high(u))).

将布尔函数表示为OBDD之后,还可以对OBDD进行简化,得到紧凑的并且唯一的图形表示.在此基础上,对于布尔函数的各种操作(例如:否定、析取、合取、存在量化、全称量化等)都可以直接通过对OBDD的操作来高效地加以实现[9].

从应用的角度来看,OBDD为集合提供了一种紧凑表示和高效操作的方式.首先,给定任一有限集合S={s1, s2,…,sn},我们可以利用二进制编码的形式,将S中的每个元素编码为=「log2n」位长的二进制串.在此基础上,将各个二进制串看成是含有个命题变量x1,x2,…,xl的布尔函数的成真赋值,则可以将S中的每个元素唯一地表示为由个命题变量构成的极小项.例如,若s1编码为00…0,s2编码为00…1,则元素s1可以由极小项m0x1∧ ¬x2∧…∧¬xl-1∧¬xl唯一表示,元素s2可以由极小项m1x1∧¬x2∧…∧¬xl-1xl唯一表示.最后,将S中各个元素对应的极小项进行析取,便得到集合S所对应的布尔函数Δ(x1,x2,…,xl).

接下来,可以根据布尔函数构造出相应的OBDD,使得对于任一极小项mi来说:mi对应的元素si包含在集合S中当且仅当OBDD中存在对应于mi的从根结点到终端结点1的一条路径.

最后,将集合隐式地表示为OBDD之后,关于集合的各种运算以及对集合包含等关系的判断都可以由相应的OBDD操作来高效地加以实现.例如,给定集合ST,令相应的布尔函数分别为ΔS(x1,x2,…,xl)和ΔT(x1,x2,…,xl),则集合ST的并、交和差运算分别对应于布尔运算ΔST(x1,x2,…,xl):=ΔS(x1,x2,…,xl)∨ΔT(x1,x2,…,xl),ΔST(x1,x2,…, xl):=ΔS(x1,x2,…,xl)∧ΔT(x1,x2,…,xl)和ΔS-T(x1,x2,…,xl):=ΔS(x1,x2,…,xl)∧¬(ΔT(x1,x2,…,xl)),并且有ST当且仅当ΔS-T (x1,x2,…,xl)=false,而这些布尔运算都可以由相应的OBDD操作来高效地加以实现.

在接下来的内容中,我们将从集合的角度来研究循环术语集的推理问题,进而借助OBDD实现相关推理.

2 最大不动点语义下基于OBDD的εL循环术语集推理

给定εL的任一TBox T,令GT=<Ndef,ET,LT>是T的描述图,Nrole={R1,…,Rn}是出现在T中的所有角色.在给出基于OBDD的推理算法之前,下面首先引入一些集合,并给出关于模拟关系的一个性质.

首先,为每个角色RiNrole构造相应的集合SR2={(u,v)∈NdefxNdef|(u,Ri,v)∈ET}.

在此基础上,依次进行以下操作:

(1) 构造集合Sold:={(v1,v2)∈NdefxNdef|L1(v1)⊆L2(v2)};

(2) 对于每个角色Ri(1≤in),依次求出如下两个集合:

· ERi:={(v'1,v2)∈NdefxNdef|存在v'2Ndef使得(v2,v'2)∈SRi并且(v1,v'2)∈Sold};

· ARi:={(v1,v2)∈NdefxNdef|对于任意v'1Ndef:如果(v1,v'1)∈SRi,则必然有(v1,v2)∈RRi};

(3) 令集合BT:=Sold∩AR1∩...∩ARn

(4) 如果BT=Sold,则返回BT,操作结束;否则,令Sold:=BT,跳转到步骤(2).

定理3. 令BT是上述算法返回的集合,则BTGTGT的最大模拟关系,即:

(1) BTGTGT的模拟关系;

(2) 对于GTGT的任一模拟关系Z,都有ZBT.

证明:令BT_k,Sold_k,ERi_k,ARi_k(k≥1)分别是步骤(3)第k次执行结束时集合BT,Sold,ERi和ARi的值.显然,BT_k

BT_k-1⊆…⊆BT_1Sold_1.即,对于任一元素(v1,v2)∈BT_k都有L1(v1)⊆L2(v2).

令算法停止时对步骤(3)总共执行了m次,则有BT=BT_m=Sold_m,因此有BT=BT∩AR1_m∩...∩ARn_m,进而有BT⊆AR1_m∩...∩ARn_m其中,

· ARi_m={(v1,v2)∈NdefxNdef|对于任意v'1Ndef:如果(v1,v'1)∈SRi,则必然有(v'1,v2)∈ERi_m}

· ERi_m={(v'1,v2)∈NdefxNdef|存在v'2Ndef使得(v2,v'2)∈SRi并且(v'1,v'2)∈BT}.

因此,对于任一元素(v1,v2)∈BT,必然有L1(v1)⊆L2(v2);并且,对于任一角色Ri(1≤in)和任一结点v'1Ndef,如果(v1,Ri,v'1)∈ET,则必然存在某个结点v'2Ndef使得(v2,Ri,v'2)∈ET并且(v'1,v'2)∈BT.根据定义4,BTGTGT的一个模拟关系.

Z是从GTGT的任一模拟关系,根据定义4,必然有Z⊆{(v1,v2)∈NdefxNdef|L1(v1)⊆L2(v2)},即ZSold_1.假设Z不包含于BT,则必然存在某个正整数≥1使得ZSold_Z不包含于Sold_+1,进而必然存在某个二元组(v1,v2)∈Z使得(v1,v2)∈Sold_但(v1,v2)∉Sold_+1.又根据算法有Sold_+1=Sold_∩AR1_∩...∩ARn_,因此必然存在某个角色Ri使得(v1,v2)∉ARn_,进而必然存在某个v'1Ndef使得(v1,v'1)∈SRi但(v'1,v2)∉ERn_,即存在某个v'1Ndef使得(v1,Ri,v'1)∈ET但不存在结点v'2Ndef使得(v2,Ri,v'2)∈ET和(v'1,v'2)∈Sold_.又由于ZSold_,因此对于二元组(v1,v2)∈Z,存在某个v'1Ndef使得(v1,Ri,v'1)∈ET,但不存在结点v'2Ndef使得(v2,Ri,v'2)∈ET和(v'1,v'2)∈Z.根据定义4,Z不是GTGT的模拟关系,产生矛盾.因此得证ZBT.

基于定理3,我们可以给出最大不动点语义下借助OBDD判断概念包含关系的算法.

算法1. 给定εL的任一TBox T,按如下步骤判断T中被定义的概念之间是否存在最大不动点语义下的包含关系:

(1) 构造出T的描述图GT=<Ndef,ET,LT>;

(2) 通过以下步骤求出GTGT的最大模拟关系:

① 令集合Ndef的元素个数为k,用=「log2k」位长的二进制串对集合Ndef中的元素进行编码,进而用含有个命题变量的极小项对集合Ndef中的各元素进行唯一的表示;

② 针对每个角色RiNrole,分别用命题变量x1,x2,…,xl构成的极小项和命题变量y1,y2,…,yl构成的极小项来唯一表示集合SRi={(u,v)∈NdefxNdef|(u,Ri,v)∈ET}中各元素的第1元和第2元,进而将集合SRi表示为布尔函数ΔRi(x1,...,xl,y1,...,yl):{0,1}x{0,1}→{0,1},使得:

③ 基于上述编码方式对集合Sold={(v1,v2)∈NdefxNdef|LT(v1)⊆LT(v2)}中的元素进行编码,并构造相应的极小项,得到集合Sold的布尔函数Δold(x1,...,xl,y1,...,yl):{0,1}lx{0,1}l→{0,1},使得:

④ 针对每个角色Ri,求出与集合ERi对应的布尔函数:

在此基础上,求出与集合对应的布尔函数:

⑤ 求出布尔函数:

⑥ 若ΔT(x1,...,xl,y1,...,yl)≠Δold(x1,...,xl,y1,...,yl),则令Δold(x1,...,xl,y1,...,yl):=ΔT(x1,...,xl,y1,...,yl),并且跳转到步骤④继续执行;

(3) 对于任意两个被定义的概念A,B,将集合{(B,A)}表示为布尔函数Δ{(B,A)}(x1,...,xl,y1,...,yl).如果Δ{(B,A)}(x1,...,xl,y1,...,yl)∧¬ΔT(x1,...,xl,y1,...,yl)=false,则返回“Agfp,TB”;否则,返回“Agfp,TB”.

上述算法中,对布尔函数的表示和运算都直接通过OBDD来实现.

下面通过一个例子来说明上述算法.

例2:对于TBox T={AP1,BP1ΠP2,CP3Π彐R.BΠ彐R.D,DP3ΠP4Π彐R.CΠ彐R.A},在最大不动点语义下判断DC之间是否存在包含关系,BA之间是否存在包含关系.

首先构造出T的描述图GT=<Ndef,ET,LT>,如图 2所示.

Fig. 2 Description graph corresponding to the TBox T in Example 2 图 2 例2中TBox T的描述图

由于TBox中总共有4个被定义的概念,可以用长度为=「log2 4」=2的二进制串对4个被定义的概念进行编码.令A编码为00(对应的极小项为¬x1∧¬x2),B编码为01(对应的极小项为¬x1x2),C编码为10(对应的极小项为x1∧¬x2),D编码为11(对应的极小项为x1x2).

由于TBox中只有一个角色R,由描述图GT可得SR={(D,A),(C,D),(C,B),(D,C)}.对集合SR中元素的第1元和第2元分别用命题变量x1,x2构成的极小项和命题变量y1,y2构成的极小项表示,可以得到:

ΔR(x1,x2,y1,y2):=(x1x2∧¬y1∧¬y2)∨(x1∧¬x2y1y2)∨(x1∧¬x2∧¬y1y2)∨(x1x2y1∧¬y2)

                        :=(x1x2∧¬y2)∨(x1∧¬x2y2).

由描述图GT可得Sold={(v1,v2)∈NdefxNdef|L1(v1)⊆L2(v2)}={(A,A),(B,B),(C,C),(D,D),(C,D),(A,B)},转换为布尔函数并化简后可得:

Δold(x1,x2,y1,y2):=(¬x1∧¬x2∧¬y1)∨(¬x1x2∧¬y1y2)∨(x1∧¬x2y1)∨(x1x2y1y2).

对于角色R,依次构造出与集合ER和集合AR相对应的布尔函数DE_RΔA_R,如下所示:

ΔE_R(z1,z2,y1,y2):=彐u1u2(ΔR(y1,y2,u1,u2)∧Δold(z1,z2,u1,u2)):=(¬z2y1y2)∨(y1∧¬y2);

ΔA_R(x1,x2,y1,y2):=∀z1z2(ΔR(x1,x2,z1,z2)→ΔE_R(z1,z2,y1,y2)):= ¬x1∨(x2y1)∨(y1∧¬y2).

接下来计算ΔT:

ΔT(x1,x2,y1,y2):=Δold(x1,x2,y1,y2)∧ΔA_R(x1,x2,y1,y2)

                        :=(¬x1∧¬x2∧¬y1)∨(¬x1x2∧¬y1y2)∨(x1∧¬x2y1∧¬y2)∨(x1x2y1y2).

由于ΔTΔold,所以令Δold:=ΔT,跳转到步骤④进行第2次迭代.

第2次执行步骤④后可得:

ΔE_R(z1,z2,y1,y2):=(¬z2y1y2)∨(z2y1∧¬y2)∨(¬z1∧¬z2y1∧¬y2),

ΔA_R(x1,x2,y1,y2):=¬x1∨(x2y1y2)∨(¬x2y1∧¬y2).

接下来执行步骤⑤后可得:

ΔT(x1,x2,y1,y2):=((¬x1∧¬x2∧¬y1)∨(¬x1x2∧¬y1y2)∨(x1∧¬x2y1∧¬y2)∨(x1x2y1y2)).

此时有ΔT=Δold,不再进行循环,算法将执行步骤(3).

假设需要判断概念C在最大不动点语义下是否包含于概念D.根据步骤(3),首先将集合{(D,C)}表示为布尔函数得到Δ{(D,C)}(x1,x2,y1,y2):=x1x2y1∧¬y2;由于Δ{(D,C)}(x1,x2,y1,y2)∧¬ΔT(x1,x2,y1,y2)=x1x2y1∧¬y2≠false,因此得到结论“Cgfp,TD”.类似地,对于本例还可以得到Agfp,TB,Bgfp,TADgfp,TC等结论.

为了表述简洁,上面例子中仅从布尔函数的层面对计算过程进行了考察.在实际计算时,对布尔函数的表示和操作实际上都是借助OBDD来实现的,其中,与布尔函数ΔR,ΔoldΔT对应的OBDD如图 3所示.

Fig. 3 OBDDs corresponding to ΔR, Δold and ΔT 图 3 ΔR,ΔoldΔT对应的OBDD

3 最小不动点语义下基于OBDD的εL循环术语集推理

给定εL的任一TBox T,令GT=<Ndef,ET,LT>是T的描述图.由定理2可知,为了在最小不动点语义下判断概念之间的包含关系,首先需要求出集合CycT.下面借助OBDD对集合CycT进行求解.

首先,根据CycT的定义,我们关注的仅仅是图GT中结点之间的连接关系,而对GT中各条边上标记的角色名并不关心.因此,我们可以去掉ET中出现的角色名,得到集合E={(v,v')|存在某个角色R使得(v,R,v')∈ET}.应用第2节的编码方法,将集合E表示为布尔函数ΔE(x1,...,xl,y1,...,yl).

其次,对于任一集合SNdef,我们用Pre(S)表示集合S中的元素在图GT中的直接前驱结点,即Pre(S)={vNdef|存在v'S使得(v,v')∈ε}.令对集合S编码后得到布尔函数ΔS(z1,...,zl),则与Pre(S)相对应的布尔函数ΔPre(S)(x1,...,xl)可由下述公式计算出来:

ΔPre(S)(x1,...,xl):=彐(z1,...,zl)(ΔS(z1,...,zl)∧ΔE(x1,...,xl,z1,...,zl)).

第三,对于任一结点vNdef,我们用集合Front(v)表示图GT中可以到达v的所有结点,用Back(v)表示图GT中从v出发可以到达的所有结点,即.令结点v编码后对应的布尔函数为Δ{v}(z1,...,zl),则与集合Front(v)对应的布尔函数ΔFront(v)(x1,...,xl)可由下列操作计算出来:

ΔTemp(x1,...,xl):=彐(z1,...,zl)(Δ{v}(z1,...,zl)∧ΔE(x1,...,xl,z1,...,zl));

ΔFront(v)(x1,...,xl):=ΔTemp(x1,...,xl)∨彐(z1,...,zl)(ΔTemp(z1,...,zl)∧ΔE(x1,...,xl,z1,...,zl));

③ 若ΔFront(v)(x1,...,xl)≠ΔTemp(x1,...,xl),则令ΔTemp(x1,...,xl):=ΔFront(v)(x1,...,xl),并跳转到步骤②;

否则,返回ΔFront(v)(x1,...,xl).

类似地,与集合Back(v)对应的布尔函数ΔBack(v)(x1,...,xl)可通过以下操作求出:

ΔTemp(x1,...,xl):=彐(z1,...,zl)(Δ{v}(z1,...,zl)∧ΔE(z1,...,zl,x1,...,xl));

ΔBack(v)(x1,...,xl):=ΔTemp(x1,...,xl)∨彐(z1,...,zl)(ΔTemp(z1,...,zl)∧ΔE(z1,...,zl,x1,...,xl));

③ 若ΔBack(v)(x1,...,xl)≠ΔTemp(x1,...,xl),则令ΔTemp(x1,...,xl):=ΔBack(v)(x1,...,xl),并跳转到步骤②;

否则,返回ΔBack(v)(x1,...,xl).

第四,定义集合Scc:={B|BNdef并且}.令对集合Ndef编码后得到布尔函数ΔN(x1,...,xl),则可通过以

下操作求出与集合Scc对应的布尔函数ΔScc(x1,...,xl):

ΔScc(x1,...,xl):=false;

ΔTemp(x1,...,xl):=ΔN(x1,...,xl);

③ 设SΔTemp(x1,...,xl)表示的集合,从中随机选取一个结点v,求出与集合{v}对应的布尔函数Δ{v}(x1,...,xl),

ΔTemp(x1,...,xl):=ΔTemp(x1,...,xl)∧¬Δ{v}(x1,...,xl);

④ 求出ΔFront(v)(x1,...,xl)和ΔBack(v)(x1,...,xl);若ΔFront(v)(x1,...,xl)∧ΔBack(v)(x1,...,xl)≠false,则令

ΔScc(x1,...,xl):=ΔScc(x1,...,xl)∨Δ{v}(x1,...,xl)∨(ΔFront(v)(x1,...,xl)∧ΔBack(v)(x1,...,xl)),

并且令

ΔTemp(x1,...,xl):=ΔTemp(x1,...,xl)∧¬(ΔFront(v)(x1,...,xl)∧ΔBack(v)(x1,...,xl));

⑤ 若ΔTemp(x1,...,xl)≠false,则跳转到步骤③;否则,算法结束,返回ΔScc(x1,...,xl).

最后,可以通过以下步骤计算出与集合CycT对应的布尔函数ΔCyc(x1,...,xl):

ΔCyc(x1,...,xl):=ΔScc(x1,...,xl);

ΔTemp(x1,...,xl):=ΔScc(x1,...,xl);

③ 设SΔTemp(x1,...,xl)表示的集合,求出ΔPre(S)(x1,...,xl),令ΔCyc(x1,...,xl):=ΔCyc(x1,...,xl)∨ΔPre(S)(x1,...,xl);

④ 若ΔCyc(x1,...,xl)≠ΔTemp(x1,...,xl),则令ΔTemp(x1,...,xl):=ΔCyc(x1,...,xl),跳转到步骤③;

否则,算法结束,返回ΔCyc(x1,...,xl).

在上述操作的基础上,基于定理2,我们可以给出最小不动点语义下借助OBDD判断包含关系的算法.

算法2. 给定εL的任一TBox T,按如下步骤判断T中被定义的概念之间是否存在最小不动点语义下的包含关系:

(1) 构造出T的描述图GT=<Ndef,ET,LT>;

(2) 令集合Ndef的元素个数为k,用=「log2k」位长的二进制串对集合Ndef中的元素进行编码,进而用含有个命题变量的极小项对集合Ndef中的各元素进行唯一表示;在该编码的基础上,借助OBDD实现以下操作:

① 求出与集合CycT对应的布尔函数ΔCyc(x1,...,xl);

② 针对每个角色RiNrole,首先利用编码的形式构造出与集合SRi={(u,v)∈NdefxNdef|(u,Ri,v)∈ET}对应的布尔函数ΔRi(x1,...,xl,y1,...,yl).在此基础上,求出布尔函数Δ'Ri(x1,...,xl,y1,...,yl):=(x1,...,xl,y1,...,yl)∧¬ΔCyc(x1,...,xl)∧¬ΔCyc(y1,...,yl),其中的ΔCyc(x1,...,xl)和ΔCyc(y1,...,yl)表示将ΔCyc(z1,...,zl)中的变量分别置换为(x1,...,xl)和(y1,...,yl);

③ 利用编码的形式构造出与集合Sold:={(L1,L2)∈NdefxNdef|λ1(v1)⊆λ2(v2)}对应的布尔函数Δold(x1,...,xl,y1,...,yl).在此基础上,求出布尔函数

Δ‘old(x1,...,xl,y1,...,yl):=Δold(x1,...,xl,y1,...,yl)∧¬ΔCyc(x1,...,xl)∧¬ΔCyc(y1,...,yl);

④ 针对每个角色Ri,首先求出布尔函数

Δ‘E_Ri(z1,...,zl,y1,...,yl):=彐(u1,...,ul)(Δ‘Ri(y1,...,yl,u1,...,ul)∧Δ‘old(z1,...,zl,u1,...,ul)),

然后求出布尔函数

⑤ 求出布尔函数

⑥ 如果,则令,并且跳转到步骤④继续执行;

(3) 对于T中任意两个被定义的概念A,B,将集合{A},{B},{(B,A)}分别表示为布尔函数Δ{A}(z1,...,zl), Δ{B}(z1,...,zl)和Δ{(B,A)}(x1,...,xl,y1,...,yl);如果Δ{A}(z1,...,zl)∧¬ΔCyc(z1,...,zl)=false,或者Δ{A}(z1,...,zl)∧¬ ΔCyc(z1,..., zl)≠false并且有Δ{B}(z1,...,zl)∧¬ΔCyc(z1,...,zl≠false和Δ{(B,A)}(x1,...,xl,y1,...,yl)∧¬Δ‘T(x1,...,xl,y1,...,yl)=false,则返回“Alfp,TB”,其他情况都返回“Alfp,TB”.

上述算法中,对布尔函数的表示和运算都直接通过OBDD来实现.

下面通过一个例子来说明上述算法.

例3:对于例2给出的TBox T,在最小不动点语义下判断ΔC之间是否存在包含关系,BA之间是否存在包含关系.

首先,构造出T的描述图GT=<Ndef,ET,LT>,与例2中相同;其次,采用与例2相同的形式对Ndef中的元素进行编码;接下来,计算与集合CycT对应的布尔函数ΔCyc.

在计算ΔCyc的过程中,首先将得到与集合Ndef对应的布尔函数ΔN(x1,x2):=true,以及与集合E={(v,v')|存在某个角色R使得(v,R,v')∈ET}={(D,A),(D,C),(C,D),(C,B)}对应的布尔函数ΔE(x1,x2,y1,y2):=(x1x2∧¬y2)∨(x1∧¬x2y2).通过多次迭代,将得到与集合Scc:={B|BNdef并且}对应的布尔函数ΔScc(x1,x2):=x1.最终,可以得到与集合CycT对应的布尔函数ΔCyc(x1,x2):=x1.

针对角色R,与例2相同,可以将集合SR表示为布尔函数ΔR(x1,x2,y1,y2):=(x1x2∧¬y2)∨(x1∧¬x2y2).在此基础上,得到布尔函数ΔR'(x1,x2,y1,y2):=ΔR(x1,x2,y1,y2)∧¬ΔCyc(x1,x2)∧¬ΔCyc(y1,y2):=false.

对于集合Sold:={(v1,v2)∈NdefxNdef|L1(v1)⊆L2(v2)},首先得到与例2相同的布尔函数:

Δold(x1,x2,y1,y2):=(¬x1∧¬x2∧¬y1)∨(¬x1x2∧¬y1y2)∨(x1∧¬x2y1)∨(x1x2y1y2).

在此基础上,得到布尔函数

(x1,x2,y1,y2):=Δold(x1,x2,y1,y2)∧¬ΔCyc(x1,x2)∧¬ΔCyc(y1,y2):=(¬x1∧¬x2∧¬y1)∨(¬x1x2∧¬y1y2).

对于角色R,依次构造出布尔函数,如下所示:

接下来,计算出布尔函数:

由于Δ'T=Δ'old,不再进行循环,算法将执行步骤(3).

假设需要判断概念C在最小不动点语义下是否包含于概念Δ.根据步骤(3),将集合{C}表示为布尔函数,得到ΔC(x1,x2):=x1∧¬x2;由于ΔC(x1,x2)∧¬ΔCyc(x1,x2)=(x1∧¬x2)∧¬x1=false,因此得到结论“Clfp,TD”.类似地,可以得到结论“Dlfp,TC”.

假设需要判断最小不动点语义下概念A与概念B之间的包含关系.根据步骤(3),将集合{A},{B},{(A,B)}, {(B,A)}分别表示为布尔函数后得到ΔA(x1,x2):=¬x1∧¬x2,ΔB(x1,x2):=¬x1x2,Δ{(A,B)}(x1,x2,y1,y2):=¬x1∧¬x2∧¬y1y2Δ{(B,A)}(x1,x2,y1,y2):=¬x1x2∧¬y1∧¬y2.

由于ΔA(x1,x2)∧¬ΔCyc(x1,x2)=¬x1∧¬x2≠false,ΔB(x1,x2)∧¬ΔCyc(x1,x2)=¬x1x2≠false,Δ{(A,B)}(x1,x2,y1,y2)∧¬Δ’T(x1, x2,y1,y2)=false和Δ{(B,A)}(x1,x2,y1,y2)∧¬Δ’T(x1,x2,y1,y2)=¬x1x2∧¬y1∧¬y2≠false,因此可以得到结论“Blfp,TA”和“Alfp,TB”.

为了表述简洁,上面例子中,从布尔函数的层面对计算过程进行了考察.在实际计算时,对布尔函数的表示和操作都是借助OBDD来实现的,其中,与布尔函数ΔCyc,Δ’R,Δ’oldΔ’T对应的OBDD如图 4所示.

Fig. 4 OBDDs corresponding to ΔCyc, Δ’R, Δ’oldand Δ’T 图 4 ΔCyc,Δ’R,Δ’oldΔ’T对应的OBDD

4 算法分析

本节首先对算法的正确性进行论证;然后,对算法的时间复杂度进行考察;最后,通过开发推理机对算法的实际计算性能进行考察.

定理4. 给定εL的任一TBox TT中任意两个被定义的概念A,B,算法1返回“Agfp,TB”当且仅当在最大不动点语义下A包含于B.

证明:令BT是算法1结束时布尔函数Δ{(B,A)}(x1,...,xl,y1,...,yl)所表示的集合,由定理3可得,BTGTGT的最大模拟关系.在此基础上,

· 一方面,如果算法1返回“Agfp,TB”,则有Δ{(B,A)}(x1,...,xl,y1,...,yl)∧¬ΔT(x1,...,xl,y1,...,yl)=false,即{(B,A)}⊆BT.

由定理1可得,在最大不动点语义下A包含于B;

· 另一方面,如果最大不动点语义下A包含于B,则根据定理1,存在模拟关系Z使得(B,A)∈Z;又由于BT是最大模拟关系,因此有ZBT,进而有{(B,A)}⊆BT.因此,算法将返回“Agfp,TB”.

定理5. 给定εL的任一TBox TT中任意两个被定义的概念A,B,算法2返回“Alfp,TB”当且仅当在最小不动点语义下A包含于B.

证明:首先考察布尔函数ΔScc(x1,...,xl)和ΔCyc(x1,...,xl)的计算过程.对于任一结点vNdef,根据对集合FrontT(v)和BackT(v)的定义,{v}∪(BackT(v)∩FrontT(v))(即Δ{v}(x1,...,xl)∨(ΔFront(v)(x1,...,xl)∧ΔBack(v)(x1,...,xl)))恰好是由含有v的且不是孤立点的强连通分支中所有结点组成的集合.因此,对ΔScc(x1,...,xl)的计算过程恰好求出了集合Scc={B|BNdef并且},而对ΔCyc(x1,...,xl)的计算过程则恰好求出了集合CycT.在此基础上,与算法1相比,算法2在步骤②和步骤③中通过合取布尔函数¬ΔCyc(x1,...,xl)∧¬ΔCyc(y1,...,yl)删除了描述图中出现在CycT中的所有结点以及与这些结点关联的所有边.基于定理2和定理4,显然定理5成立.

定理6. 给定εL的任一TBox T,令其描述图为GT=<Ndef,ET,LT>,则算法1的时间复杂度为O(|NR|x|Ndef|2).

证明:首先,集合Sold={(v1,v2)∈NdefxNdef|LT(v1)⊆LT(v2)}的元素个数最多为|Ndef|2,因此,算法1中步骤④与步骤⑥之间的循环最多为|Ndef|2次;其次,每次执行步骤④时,需要为每个角色Ri都计算一次布尔函数ΔE_Ri(z1,...,zl, y1,...,yl)和ΔA_Ri(x1,...,xl,y1,...,yl);最后,对于布尔函数的析取、合取、量化等操作,可以借助OBDD在恒定时间内完成.因此,总的来说,算法1的时间复杂度为O(|NR|x|Ndef|2).

定理7. 给定εL的任一TBox T,令其描述图为GT=<Ndef,ET,LT>,则算法2的时间复杂度为O(|NR|x|Ndef|2).

证明:与算法1相比,算法2增加的时间开销主要体现在对布尔函数ΔCyc(x1,...,xl)的计算上,而计算ΔCyc(x1,..., xl)的时间又主要花费在对布尔函数ΔScc(x1,...,xl)的计算上.下面来考察ΔScc(x1,...,xl)的计算过程.首先,步骤③与步骤⑤之间的循环最多为|Ndef|次;其次,每次执行步骤④计算ΔFront(v)(x1,...,xl)(或ΔBack(v)(x1,...,xl))时,需要调用布尔函数ΔFront(v)(x1,...,xl)(或ΔBack(v)(x1,...,xl))的计算过程,在该计算过程中,最多又需要进行|Ndef|次循环.因此总的来说,计算ΔScc(x1,...,xl)的时间复杂度为O(|Ndef|2).因此,计算ΔCyc(x1,...,xl)的时间复杂度也为O(|Ndef|2).再综合定理6可得,算法2的时间复杂度为O(|NR|x|Ndef|2).

上述关于时间复杂度的结论与Baader等人[6]给出的结论相一致.

为了从实际计算性能的角度对基于OBDD的推理算法进行考察,我们采用Java语言并且调用JavaBDD (http://javabdd.sourceforge.net/)类库中关于OBDD的操作函数实现了本文给出的两种算法,开发了基于OBDD的εL循环术语集推理机.推理机以OWL语言表示的εL知识库作为输入,计算出被定义的概念之间存在的所有包含关系,同时给出整个过程所花费的时间.

由于找不到既含有循环定义又不超过描述逻辑εL刻画能力的本体测试用例,我们以本文例2中的循环术语集作为基本测试用例.例2的循环术语集只含有8个概念名和1个角色.为了增大本体规模,我们为该循环术语集不断生成新的副本,将副本中的概念和角色重新命名(例如,对于概念名A,在各个副本中依次命名为A_1, A_2,…等),然后将这些副本和原来的术语集一起构成新的本体.我们将例2中循环术语集的规模看作1个单位,每加入1个副本都增加1个单位.在此基础上,实验结果如图 5所示,其中的横坐标为本体规模,当本体规模为10时,表示该本体由例2的循环术语集及其9个副本组成,从而具有80个概念名和10个角色,依此类推.纵坐标为推理结束所需要的时间.为了实验数据的准确性,我们针对每个本体都采用运行5次后求平均值的方式得到运行时间.图中标识为“EL_gfp”的曲线是最大不动点语义下(即算法1)的实验结果,标识为“EL_lfp”的曲线是最小不动点语义下(即算法2)的实验结果.实验平台为Thinkpad X200 PC机、Windows7 64bit操作系统、Intel Core 2 Duo P8600 CPU、4GB内存、JDK版本为1.6.

Fig. 5 Experimental comparison with Pellet 图 5 与Pellet的实验比较

为了得到关于算法性能的直观评价,我们还在同样的配置环境下用著名的描述逻辑推理机Pellet运行了各个测试用例,得到图中标识为“Pellet”的实验数据.

需要强调的是:Pellet推理机并不支持最大不动点语义下和最小不动点语义下对循环术语集的推理;将测试用例作为输入之后,Pellet推理机给出的仅仅是描述语义下的推理结果.因此,从时间性能的角度将本文的算法与Pellet推理机作比较是不合适的.但通过该实验至少可以看出,本文的算法在时间性能上是可以接受的.甚至于当本体规模小于115个单位(即920个概念名和115个角色)时,本文最大不动点语义下的推理算法所需要的时间低于目前性能最好的Pellet推理机.此外,本文基于OBDD的算法在时间性能上还有较大的提升空间:一方面,目前我们是先用显式的集合的方式计算和刻画出描述图GT,然后在算法过程中才部分地借助OBDD来表示和实现.如果一开始就借助OBDD对描述图进行求解和表示,则算法性能可以得到更大的提高;另一方面,我们在实现算法时使用了JavaBDD类库中关于OBDD的现有操作和函数,这些操作和函数的计算性能并不是最优的,从而也在一定程度上影响了本文的实验结果.

5 相关工作比较

蒋运承等人[7]将Baader[6]的工作扩展到描述逻辑εLN,将描述图和模拟关系引入到描述逻辑εLN循环术语集中;在不动点语义下,蒋运承等人研究了概念可满足性问题和概念包含问题,给出了基于描述图和模拟关系的判定算法.与该工作相比,本文采用OBDD研究循环术语集的推理问题.为了能够使用OBDD,在Baader和蒋运承等人工作的基础上,本文首先给出一条关于描述图上最大模拟关系的性质,借助集合表示和集合运算对该性质进行了表述和证明.在此基础上,本文应用布尔函数对描述图进行编码,进而基于OBDD给出了不动点语义下对概念包含关系进行判定的算法.本文的工作主要是针对Baader[6]提出的描述逻辑ελ循环术语集来进行的,但实际上,在蒋运承等人工作的基础上,可以比较容易地将本文的算法扩展到处理描述逻辑εLN循环术语集.

Pan等人[14]将BDD应用于模态逻辑K的可满足性判定.该方法可以比较容易地扩展到处理含有多个模态词的模态逻辑K(m).由于K(m)与描述逻辑ALC之间存在一一对应关系,因此,Pan等人[14]的工作实际上给出了一种对描述逻辑ALC的概念可满足性进行判定的算法.之后,Keller[15]首次明确提出了将OBDD应用于描述逻辑推理的思路:首先,将描述逻辑知识库转化为与之可满足性等价的命题逻辑公式;然后,再借助OBDD对命题公式的可满足性进行判定.然而,Keller并未给出具体的算法.Rudolph等人[16, 17]首次给出了将OBDD应用于描述逻辑推理的算法.针对描述逻辑SHIQ刻画的知识,Rudolph等人首先构造出一种称为多米诺集的结构,借助多米诺集,Rudolph等人将描述逻辑知识库转化为布尔函数表示形式,进而给出了基于OBDD的推理算法.Rudolph等人从理论上证明了算法的正确性,并对算法的复杂度进行了分析.上述3项工作为描述逻辑推理提供了一种全新的思路和途径,但与描述逻辑领域的大部分研究工作相似,他们都假设了所考察的知识库中不含有循环定义.因此与这些工作相比,本文的特点是首次将OBDD应用于描述逻辑循环术语集的推理.

6 结束语

在文献中借助描述图和模拟关系解决循环术语集推理问题的基础上,本文借助集合表示和集合运算给出描述图上关于最大模拟关系的一个重要性质,基于该性质给出了应用OBDD求解最大模拟关系的方法,进而依次给出了最大不动点语义下和最小不动点语义下借助OBDD对概念包含关系进行判定的算法.据我们所知,本文是首次将OBDD应用于描述逻辑循环术语集推理的文献.本文的工作一方面为循环术语集的推理提供了一条有效的途径,另一方面为OBDD与描述逻辑推理以及逻辑定理证明的结合提供了新的思路和案例.

下一步的工作是继续优化本文的算法.同时,对这些算法进行扩展,借助OBDD对表达能力更强的描述逻辑的循环术语集进行推理.

参考文献
[1] 史忠植,董明楷,蒋运承,张海俊.语义Web的逻辑基础.中国科学(E辑:信息科学),2004,34(10):1123-1138 .
[2] Baader F. Using automata theory for characterizing the semantics of terminological cycles. Annals of Mathematics and Artificial Intelligence, 1996,18(2-4):175-219 .
[3] Kusters R. Characterizing the semantics of terminological cycles in ALN using finite automata. In: Cohn AG, Schubert L, Shapiro SC, eds. Proc. of the 6th Int’l Conf. on Principles of Knowledge Representation and Researching.San Francisco: Morgan Kaufmann Publishers, 1998. 499-511.
[4] Nebel B. Terminological cycles: Semantics and computational properties. In: Sowa JF, ed. Proc. of the Principles of Semantic Networks. San Francisco: Morgan Kaufmann Publishers, 1991. 331-362.
[5] Nebel B. Reasoning and Revision in Hybrid Representation Systems. New York: Spring-Verlag, 1990.
[6] Baader F. Terminological cycles in a description logic with existential restrictions. In: Gottlob G, Walsh T, eds. Proc. of the 18th Int’l Joint Conf. on Artificial Intelligence. San Francisco: Morgan Kaufmann Publishers, 2003. 325-330.
[7] Jiang YC, Wang J, Shi ZZ, Tang Y. Fixpoint semantics and reasoning terminological cycles in description logic εLN.Ruan Jian Xue Bao/Journal of Software, 2009,20(3):477-490 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3215.htm
[8] 王驹,蒋运承,申宇铭.描述逻辑系统vL循环术语集的可满足性及推理机制.中国科学(F辑:信息科学),2009,39(2):205-211 .
[9] Gu TL, Xu ZB. Ordered Binary Decision Diagram and Its Applications. Beijing: Science Press, 2009 (in Chinese).
[10] Yan H, Zhang W, Zhao HY, Mei H. BDD-Based approach to the verification of feature models.Ruan Jian Xue Bao/Journal of Software, 2010,21(1):84-97 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3525.htm
[11] Uribe TE, Stickel ME. Ordered binary decision diagrams and the Davis-Putnam procedure. In: Jouannaud JP, ed. Proc. of the 1st Int’l Conf. on Constraints in Computational Logics. LNCS 845, Berlin: Springer-Verlag, 1994.34-49 .
[12] Groote JF, Tveretina O. Binary decision diagrams for first-order predicate logic. Journal of Logic and Algebraic Programming, 2003,57(1-2):1-22 .
[13] Marrero W. Using BDDs to decide CTL. In: Halbwachs N, Zuck LD, eds. Proc. of the 11th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3440, Berlin: Springer-Verlag, 2005.222-236 .
[14] Pan GQ, Sattler U, Vardi MY. BDD-Based decision procedures for the modal logic K. Journal of Applied Non-Classical Logics, 2006,16(1-2):169-208.
[15] Keller U. Towards novel techniques for reasoning in expressive description logics based on binary decision diagrams. In: Simperl EB, Diederich J, eds. Proc. of the 4th Annual European Semantic Web Conf. 2007. 435-450.
[16] Rudolph S, Krötzsch M, Hitzler P. Terminological reasoning in SHIQ with ordered binary decision diagrams. In: Fox D, Gomes CP, eds. Proc. of the 23rd National Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 2008. 529-534.
[17] Rudolph S, Krötzsch M, Hitzler P. Type-Elimination-Based reasoning for the description logic SHIQbs using decision diagrams and disjunctive datalog. Logical Methods in Computer Science, 2012,8(1):1-38 .
[7] 蒋运承,王驹,史忠植,汤庸.描述逻辑εLN循环术语集的不动点语义及推理.软件学报,2009,20(3):477-490.http://www.jos.org.cn/1000-9825/3215.htm
[9] 古天龙,徐周波.有序二叉决策图及应用.北京:科学出版社,2009.
[10] 闫华,张伟,赵海燕,梅宏.基于二分决策图的特征模型验证方法.软件学报,2010,21(1):84-97. http://www.jos.org.cn/1000-9825/3525.htm