基于描述逻辑的本体的保守扩充理论、模块抽取理论、通用模块构建理论及其相关算法是本体工程中本体构建、本体融合及重构的核心理论与工具.国际上该领域已有Lutz等人使用形式构模方法证明了ALC的保守扩充判定算法复杂度是二阶时间指数的,而轻量级的系统?L的算法复杂度是一阶时间指数的.但当前文献中的形式构模方法思路复杂,难以把握,几乎不能在实用的工程层面上实现.提出一种面向轻量级的描述逻辑系统家族(DL-Lite family)的统一的二阶线性推理机制,并给出该推理机制的完备性证明.该方法直观,思路清晰,从而在工程中容易实现.同时,该方法对εL,FL0,FLε,v L等DL-Lite家族的所有系统都有效.在该线序推理系统下,可以根据"空间换时间"的原则,设计和实现关于保守扩充判定的图推理机制,其复杂性(相对于空间的大小)是多项式的.
In the framework of description logics, the theories and their related algorithms of conservative extensions, modularity and module extraction are the core notions and vital tools in engineering semantic Web construction, ontology construction, ontology merging and reuse. Among other important contributions in this area, Lutz, et al. have shown that the conservative extension problem for ALC is decidable but its complexity is 2Exp Time-complete while the complexity of the deciding algorithm for light-weight ?L is 1Exp Timecomplete. Their deciding algorithms are basically depends on tableau algorithm which is substantially a reasoning mechanism in first-order predicate logic. Although, theoretically speaking, those results and algorithms are significant and valuable, both existing theories and methods appear to be complicated, difficult to understand, and hard to implement by engineers working on the semantic Web and ontology construction. This paper will not discuss and analyze the current theories and their algorithms. Instead, it independently proposes a second-order linear reasoning mechanism for all members of DL-Lite family. A proof of the completeness of the second-order deduction system is provided. The proposed mechanism is intuitive, easy to manipulate, and much easier to implement in the engineering sector. It is uniformly applicable for members of DL-Lite family such as εL, FL0, FLε, and v L. Most of all, this system is consistent with graph deduction that facilitates design and construction of the necessary graphs by using space to exchange with time cost. As a result, the time complexity is reduced significantly such that if the space and deduction graphs are sophisticatedly equipped, the deciding time can be reduced topolynomial.