(Non-)Succinctness of uniform interpolants of general terminologies in the description logic ELEL

ELEL is a popular description logic, used as a core formalism in large existing knowledge bases. Uniform interpolants of knowledge bases are of high interest, e.g. in scenarios where a knowledge base is supposed to be partially reused. However, to the best of our knowledge no procedure has yet been proposed that computes uniform ELEL interpolants of general ELEL terminologies. Up to now, also the bound on the size of uniform ELEL interpolants has remained unknown. In this article, we propose an approach to computing a finite uniform interpolant for a general ELEL terminology if it exists. To this end, we develop a quadratic representation of ELEL TBoxes as regular tree grammars. Further, we show that, if a finite uniform ELEL interpolant exists, then there exists one that is at most triple exponential in the size of the original TBox, and that, in the worst case, no smaller interpolants exist, thereby establishing tight worst-case bounds on their size. Beyond showing these bounds, the notions and results established in this paper also provide useful insights for designing efficient ontology reformulation algorithms, for instance, within the context of module extraction.