Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig Interpolation Property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in fourfold exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.

翻译：近期研究已确定了在缺少克雷格插值性质（CIP）的逻辑中判定插项存在性的复杂度结果。目前所发展的证明技术是非构造性的，且关于插项尺寸的有意义界限尚不可知。混合模态逻辑（或称含名称的模态逻辑）是一类特别有趣的无CIP逻辑体系：在其情形下，若要保持可判定性则无法恢复CIP，而在实际应用中这些逻辑中的插项可作为确定描述符，以及描述逻辑知识库中正负数据示例间的分隔符。本文通过一种新的超镶嵌消去技术证明，在许多标准混合模态逻辑中，若克雷格插项存在，则可在四重指数时间内计算得到。另一方面，我们证明均匀插项的存在性是不可判定的，这与模态逻辑或直觉主义逻辑（其中均匀插项始终存在）形成鲜明对比。