As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation 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完全性。