Ordered Label And Axiom Expansion Options In Ontology Debugging

The goal of the semantic web is to make information on the web understood by computerwhich semantic web is the extension of current world wide web. As the core layer of semanticweb, ontology is the formal description of shared concepts for specific areas, which ensurescommon understanding of concepts and their relationships. Description logic as the logicalfoundation of ontology with good semantic and expressive power, can provide decidablereasoning services.In the real life, ontologies constructed by experts have been widely used in variousaspects of computer science and engineering. With the continuous improvement of ontologybuilding tools, ontologies may be constructed by more non-experts, or be merged by differentdata. It may introduce inconsistence in ontologies which we can derive the conflictingknowledge from ontology easily. Also, the ontology integration, migration, evolution andother tasks of ontologies may lead to inconsistence. It means that in the entire life cycle ofontology, including construction, use, updating and maintenance, digestion for inconsistenceof knowledge is inseparable. Therefore, ontology debugging has become an important issue insemantic web.So far, existing reasonor can determine whether the concept is satisfiable only, but isunable to provide effective reference information and tell the user the reason of unsatisfiablity.This paper discusses how to solve all logical conflicts for incoherent ontology terminology.We mainly provide solutions to axiom pinpointting with extending traditional Tableaucalculus and selection function which finds out axioms to be expanded.The details are asfollows:(1) In the method of ontology debugging based on Tableau calculus with ordered label,by analyzing the reason for unsatisfiablity and inconsistency, we study correspondingrelationship between the two and the dependencies among unsatisfiable concepts, and presentan algorithm which can compute out all minimal incoherence preserving sub-TBox for anunsatisfiable concept in a ontology. In the process of Tableau calculus with ordered label foran unsatisfiable concept, we can get all the other unsatisfiable concepts among itsdependencies, which reduce the amount of calculation. We present a comparison between ouralgorithm and a current representative algorithm, and the results indicate that the Tableau calculus algorithm with ordered label is more efficientand more accurate.(2) In the method of axiom pinpointing based on axiom expansion options, we first useselection function to choose the current related axioms from terminology, and then delete theselected axiom one by one to determine the key axiom result in unsatisfiablity of concept.And the retained axiom set is a minimal unsatisfiability preserving sub-TBox. Further, wecombine the Hitting Set Tree algorithm of Reiter with depth-first principle to generate a HSTwhich contains all MUPS of an unsatisfiable concept. It can reduce the solution space ofMUPS problem.The experiment results show that the debugging method based on axiomexpansion options processes the ontologies with different expression efficiently.Both the methods proposed in this paper could pinpoint all logical conflicts forincoherent ontology, and have greater time efficiency.