Inhaltszusammenfassung

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 ≤-interpolation in classes of semilattices with monotone operators; we show, by giving a counterexample, that ≤-interpolation doe...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 ≤-interpolation in classes of semilattices with monotone operators; we show, by giving a counterexample, that ≤-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 EL and EL+. (Extended version of the CADE 2023 paper with the same title.)» weiterlesen» einklappen

Autoren

Klassifikation

DFG Fachgebiet:
Informatik

DDC Sachgruppe:
Informatik