本体作为知识库表示知识已经成为计算机理论与应用的研究热点.在描述逻辑中,将本体看作一个逻辑理论,一个本体被形式化为给定的描述逻辑系统的一个Tbox.本体是动态的实体,为了适应新领域的发展,需要对原始本体进行扩充.但是扩充后的本体与原始本体是否保持逻辑一致性是目前研究者们所关注的焦点.在Lutz等人研究的基础上探究的保守扩充问题.首先构建了的典范模型,将包含推理问题转换为典范模型的模拟问题;其次由典范模型之间的最大模拟是多项式时间复杂的,证明了的包含推理是多项式时间复杂的;最后给出描述逻辑的保守扩充及其判定算法,证明了的保守扩充的判定算法是指数时间复杂的.
Conservative extension is an important property in the mathematical logic. Its notion plays acentral role in ontology design and integration. It can be used to formalize ontology refinements,safe mergings of two ontologies, and independent modules inside an ontology. Regarding reasoning support, the most basic task is to decide whether one ontology is a conservative extension of another. If this is not the case, the evolution of the ontology with the original ontology will not be able to maintain the same logical conclusion. In recent years, lightweight description logics (DLs) have gained increasing popularity. In fact ontology is definitely the structured knowledge base in description logic. As we know, knowledge is not always the same, so it needs to be extended as long as new improvement appears in this field. It is concerned that whether it is consistent with the primitive one after extension. The conservative extension of FL0 system is analyzed based on Lutzs' work. Firstly the FL0 canonical model is constructed and the inclusion inference is reduced to the simulations between two FL0 canonical models. The complexity is pointed out to be polynomial based on the fact that the canonical models' largest simulation is polynomial. After that the FL0 conservative extension algorithm is presented and its complexity is proved to be exponential.