On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics \cal EL, \cal EL⁺

2023/07/17 by Peuter, Dennis, Sofronie-Stokkermans, Viorica, Thunert, Sebastian
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2307.08843

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 ≤-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 \sqsubseteq-interpolation in the description logics \cal EL and \cal EL⁺.

Related

• Locality and applications to subsumption testing and interpolation in EL and some of its extensions
• Uniform Interpolation
• Interpolation in model theory
• Interpolation Theorems for Nonmonotonic Reasoning Systems
• Interpolation in Non-Classical Logics