ExpExpExplosion: Uniform Interpolation in General εL Terminologies

摘要

Although εL is a popular logic used in large existing knowledge bases, to the best of our knowledge no procedure has yet been proposed that computes uniform εL interpolants of general εL terminologies. Up to now, also the bounds on the size of uniform εL interpolants remain unknown. In this paper, we propose an approach based on proof theory and the theory of formal tree languages to computing a finite uniform interpolant for a general εL terminology if it exists. Further, we show that, if such a finite uniform εL 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 shorter interpolants exist, thereby establishing the triple exponential tight bounds on their size.