On $P$-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $\mathcal{E}\mathcal{L},{\mathcal{E}\mathcal{L}}^{+}$

Abstract

We study the problem of $P$-interpolation, where $P$ is a set of binary predicate symbols, for certain classes of local extensions of a base theory. For computing the $P$-interpolating terms, we use a hierarchic approach: This allows us to compute the interpolating terms using a method for computing interpolating terms in the base theory. We use these results for proving $\le$-interpolation in classes of semilattices with monotone operators; we show, by giving a counterexample, that $\le$-interpolation does not hold if by "shared" symbols we mean just the common symbols. We use these results for the study of $⊑$-interpolation in the description logics $\mathcal{E}\mathcal{L}$ and ${\mathcal{E}\mathcal{L}}^{+}$.

33 pages