Lexicographical inference over inconsistent DL-based ontologies

Abstract

Logical inconsistency may often occur throughout the development stage of a DL-based ontology. We apply the lexicographic inference to reason over inconsistent DL-based ontologies without repairing them first. We address the problem of checking consequences in a ontology that are classically inferred from every consistent (or coherent) subontology having the highest lexicographic precedence. We propose a method for compiling a ontology to a propositional program so that the problem can be solved in polynomial calls to a SAT solver. We prove that this time complexity is worst-case optimal in data complexity. In order to make the method more scalable, we also present partition-based techniques to optimize the calling of SAT solvers. © 2008 Springer Berlin Heidelberg.