Normal modal logics extending the logic K4.3 of linear transitive frames are known to lack the Craig interpolation property, except some logics of bounded depth such as S5. We turn this `negative' fact into a research question and pursue a non-uniform approach to Craig interpolation by investigating the following interpolant existence problem: decide whether there exists a Craig interpolant between two given formulas in any fixed logic above K4.3. Using a bisimulation-based characterisation of interpolant existence for descriptive frames, we show that this problem is decidable and coNP-complete for all finitely axiomatisable normal modal logics containing K4.3. It is thus not harder than entailment in these logics, which is in sharp contrast to other recent non-uniform interpolation results. We also extend our approach to Priorean temporal logics (with both past and future modalities) over the standard time flows-the integers, rationals, reals, and finite strict linear orders-none of which is blessed with the Craig interpolation property.

翻译：已知扩展了线性传递框架逻辑K4.3的正规模态逻辑缺乏克雷格插值性质，但诸如S5等有界深度逻辑除外。我们将这一"否定性"事实转化为研究问题，采用非均匀方法研究克雷格插值，具体探究如下插值存在性问题：对于K4.3之上的任意固定逻辑，判定两个给定公式之间是否存在克雷格插值。利用描述性框架中基于互模拟的插值存在性刻画，我们证明该问题对于所有包含K4.3的有限可公理化的正规模态逻辑都是可判定的且为coNP完全的。因此，该问题并不比这些逻辑中的蕴含问题更困难，这与其他近期非均匀插值结果形成鲜明对比。我们还将该方法扩展到标准时间流（整数、有理数、实数及有限严格线性序）上的普赖尔时态逻辑（同时包含过去和未来模态算子）——这些逻辑均不具备克雷格插值性质。