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则必然牺牲可判定性；而在实际应用中，这些逻辑中的插项可作为描述逻辑知识库中的确定描述符以及正负数据样本间的分离器。本文通过新型超拼图消去技术证明，在众多标准混合模态逻辑中，若克雷格插项存在，则可在四重指数时间内完成计算。另一方面，我们证明一致插项的存在性是不可判定的，这与模态逻辑或直觉主义逻辑中一致插项必然存在的情况形成鲜明对比。