Resolving Logical Contradictions in Description Logic Ontologies Based on Integer Linear Programming

Abstract

When resolving logical contradictions in ontologies, Reiter's hitting set tree algorithm is often applied to satisfy the minimal change principle. To improve the efficiency, the researchers have proposed various algorithms by using a scoring function, defining new semantics or applying some heuristic strategies. However, these algorithms either sacrifice minimal change or are designed for less expressive ontologies like DL-Lite. In this paper, we propose a mathematic approach based on integer linear programming, which is an optimization problem of maximizing or minimizing a linear objective function, to deal with DL ontologies. Specifically, we define the integer linear programming-based model to resolve logical contradictions. To realize the model, we propose one algorithm to find a cardinality-minimal solution and two algorithms dealing with weighted ontologies. Our experiments are conducted over 70 real-life and artificial ontologies to compare our algorithms with those hitting set tree-based ones. Through the experiments, the prominent efficiency and effectiveness have been exhibited by our algorithms. They usually take about 0.4 s to find a solution while others spend more than 100 s in many cases. The experimental results also show that the first two algorithms could find the cardinality-minimal solutions and those with a minimal sum of weights, respectively.

Keywords

• Logical contradictions
• inconsistency handling
• ontology repair
• semantic web
• integer linear programming