Containing Reasoning and Its Conservative Extensionsin Description Logic FL0

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.