论文部分内容阅读
描述逻辑(DL)作为一类用于知识表示的形式化工具,具有较强的表达能力和可判定性。近年来,随着语义Web的兴起,描述逻辑成为了知识表示领域的研究热点。在关于描述逻辑的研究课题中,一个关键的问题是如何设计有效的推理算法。尽管Tableau-算法在描述逻辑推理中得到了广泛并且成功的应用,但寻求更好的推理算法一直是学术界和工业界关注的问题。 有序二叉决策图(OBDD)是一种基于图的数据结构,它是布尔函数的一种压缩表示形式。由于有序二叉决策图能有效地表示和处理布尔函数,因此在大规模模型检测和验证等领域已经得到了成功应用。针对OBDD的数据结构特点,本文基于OBDD实现了对εL(┐)本体和ALCIO本体的一致性判定。其研究内容和主要贡献如下: (1)给出了基于OBDD的εL(┐)本体判定算法。首先,利用标准化规则对TBox进行化简;然后,重构了知识库TBox模型,进而将该模型转化为满足3CNF约束(每个从句含有三个变元的合取范式)的布尔函数;最后,利用OBDD的可满足性操作对布尔函数进行判定。 (2)给出了基于OBDD的ALICO本体判定算法,实现了对Nominals推理。首先,利用NNF变换和FLAT++规则对TBox进行化简;然后,通过模型重构将TBox转化为相应的布尔函数;最后,将布尔函数表示成OBDD,进而进行一致性判定,从理论上证明了算法的完备性、可靠性和可终止性。 (3)针对以上两种推理算法,开发了相应的原型推理系统:DLROBDD-3CNF(EL(┐))和DLROBDD(ALCIO)。实验结果表明,就DLROBDD-3CNF(EL(┐))而言,利用标准化规则和过程优化确实有效地提高了算法的时间性能。尽管DLROBDD(ALCIO)不能在所有案例推理时均优于基于Tableau-算法的Pellet推理系统,但在实际应用中,其性能仍具有竞争力。实验结果还表明,与Tableau-算法相比,本体中角色名数量越少或者选择的变量序越优,基于OBDD的描述逻辑推理算法的优越性就越为明显。