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

TL;DR

This paper investigates P-interpolation in local theory extensions, providing a hierarchic approach for computing interpolants and applying these results to description logics ${ m EL}$ and ${ m EL}^+$, with implications for logical inference.

Contribution

It introduces a hierarchic method for P-interpolation in local theory extensions and applies it to description logics, establishing new results and counterexamples.

Findings

Hierarchic approach enables computation of interpolants in base theories.

$ extless$-interpolation holds in semilattices with monotone operators.

Counterexample shows $ extless$-interpolation fails with only shared symbols.

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 $\leq$-interpolation in classes of semilattices with monotone operators; we show, by giving a counterexample, that $\leq$-interpolation does not hold if by "shared" symbols we mean just the common symbols. We use these results for the study of $\sqsubseteq$-interpolation in the description logics ${\cal EL}$ and ${\cal EL}^+$.