Journal of Software:2017.28(2):216-233

(广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;黔南民族师范学院 数学系, 贵州 都匀 558000)
Second-Order Linear Reasoning Mechanisms for Description Logic εL
WANG Ju,CHEN Guang-Xi,YU Quan
(Guangxi Key Laboratory of Trusted Software(Guilin University of Electronic Technology), Guilin 541004, China;Department of Mathematics, Normal College of Minorities of South Guizhou, Duyun 558000, China)
Chart / table
Similar Articles
Article :Browse 1352   Download 1024
Received:August 20, 2015    Revised:October 17, 2015
> 中文摘要: 基于描述逻辑的本体的保守扩充理论、模块抽取理论、通用模块构建理论及其相关算法是本体工程中本体构建、本体融合及重构的核心理论与工具.国际上该领域已有Lutz等人使用形式构模方法证明了ALC的保守扩充判定算法复杂度是二阶时间指数的,而轻量级的系统εL的算法复杂度是一阶时间指数的.但当前文献中的形式构模方法思路复杂,难以把握,几乎不能在实用的工程层面上实现.提出一种面向轻量级的描述逻辑系统家族(DL-Lite family)的统一的二阶线性推理机制,并给出该推理机制的完备性证明.该方法直观,思路清晰,从而在工程中容易实现.同时,该方法对εL,FL0,FLε,vL等DL-Lite家族的所有系统都有效.在该线序推理系统下,可以根据“空间换时间”的原则,设计和实现关于保守扩充判定的图推理机制,其复杂性(相对于空间的大小)是多项式的.
Abstract: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 2ExpTime-complete while the complexity of the deciding algorithm for light-weight εL is 1ExpTime-complete. 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 vL. 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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61463044,61363030);广西自然科学基金(2013GXNSFAA019330);广西可信软件重点实验室开放基金;桂林电子科技大学计算机软件创新团队基金(kx201419);广东省数学教育工程技术研究中心开放基金 国家自然科学基金(61463044,61363030);广西自然科学基金(2013GXNSFAA019330);广西可信软件重点实验室开放基金;桂林电子科技大学计算机软件创新团队基金(kx201419);广东省数学教育工程技术研究中心开放基金
Foundation items:Natural Science Foundation of China (61463044, 61363030); Natural Science Foundation of Guangxi Province of China (2013GXNSFAA019330), Open Foundation of Guangxi Key Laboratory of Trusted Software; Foundation of Software Innovative Teamof Guilin University of Electronic Technology (kx201419); Foundation of Guangdong Province Engineering Technology Research Center for Mathematical Educational Software
Reference text:


WANG Ju,CHEN Guang-Xi,YU Quan.Second-Order Linear Reasoning Mechanisms for Description Logic εL.Journal of Software,2017,28(2):216-233