Deciding Subsumers of Least Fixpoint Concepts w.r.t. general EL -TBoxes.
Shasha Feng, Michel Ludwig, Dirk Walther · 2015
In this paper we provide a procedure for deciding subsumptions of the form T |= C v E, where C is an ELUμ-concept, E an ELUconcept and T a general EL-TBox. Deciding such subsumptions can be used for computing the logical difference between general EL-TBoxes. Our procedure is based on checking for the existence of a certain simulation between hypergraph representations of the set of subsumees of C and of E w.r.t. T , respectively. With the aim of keeping the procedure implementable, we provide a detailed construction of such hypergraphs deliberately avoiding the use of intricate automata-theoretic techniques.