Concept Definability and Interpolation in Enriched Models of EL-TBoxes.
Denis K. Ponomaryov, Dmitry Vlasov · 2013
Abstract. It is known that in Description Logics explicit concept definability is directly related to concept interpolation. The problem to decide whether a concept is definable under a TBox wrt a signature usually reduces to entailment in the underlying logic. If an explicit definition exists, then it can be found as a concept interpolant for a concept inclusion entailed by an appropriately chosen TBox. In fact, it can be extracted from a corresponding proof of the concept inclusion. We describe a graph structure called enriched model that represents proofs in normalized EL-TBoxes and show that, built once for a normalization of a given TBox T, it can be used for deciding the existence or direct computation of explicit definitions of concepts under arbitrary subsets of axioms of T and wrt different subsignatures of T. Solving this computational problem has applications in collaborative ontology engineering and is an important part of the recently proposed algorithms for ontology decomposition.