混合模态逻辑的插值计算与规模

近期研究在缺乏克雷格插值属性（CIP）的逻辑中，确立了决定插值是否存在的复杂性结果。迄今为止的证明技术均为非构造性，关于插值规模的有意义界限尚未知晓。混合模态逻辑（或带有名词的模态逻辑）是一类特别有趣的逻辑，因其 lacking CIP：在不牺牲可判定性和在实际应用中，这些逻辑的插值可作为 definite descriptions 在描述逻辑知识库中作为正负数据示例之间的分离符。本文我们提出一种新型的超马赛克消除技术，展示在许多标准混合模态逻辑中，克雷格插值可在四倍指数时间内计算（若存在）。另一方面，我们证明统一插值存在性不可判定，这与模态逻辑或直觉主义逻辑中统一插值总是存在的结论形成鲜明对比。