An automata-theoretic approach to uniform interpolation and approximation in the description logic EL
Carsten Lutz, İnanç Seylan, Frank Wolter · 2012
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 modeltheoretic 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. 1