An Automata-Theoretic Approach to Uniform Interpolation and Approximation in the Description Logic EL.

We study (i) uniform interpolation for TBoxes that are formulated in the lightweight description logic EL and (ii) EL-approximations of TBoxes formulated in more expressive languages. In both cases, we give model-theoretic characterizations based on simulations and cartesian products, and we develop algorithms that decide whether interpolants and approximants exist. We present a uniform approach to both problems, based on a novel amorphous automaton model called EL automata (EA). Using EAs, we also establish a simpler proof of the known result that conservative extensions of EL -TBoxes can be decided in EXPTIME.