As well known, weak K4 and the difference logic DL do not enjoy the Craig inter- polation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the nonexistence of an interpolant can always be witnessed by a pair of bisimilar models of polynomial size for DL and of triple-exponential size for weak K4, and so the interpolant existence problems for these logics are decidable in coNP and coN3ExpTime, respectively. We also establish coNExpTime-hardness of this problem for weak K4, which is higher than the PSpace-completeness of its decision problem.

翻译：众所周知，弱K4逻辑与差异逻辑DL并不具备克雷格内插性质。本文关注的是判定任意给定蕴含式在这两种逻辑中是否存在内插项的问题。研究表明，内插项的不存在性可通过一对双模拟模型来证否：对于DL，这对模型具有多项式规模；对于弱K4，则具有三指数规模。由此得出，这两种逻辑的内插存在性问题的可判定性分别属于coNP和coN3ExpTime复杂度类。此外，我们还证明了弱K4的该问题具有coNExpTime难度——这高于其判定问题的PSpace完全性。