The interpolant existence problem for weak K4 and difference logic
Agi Kurucz, Frank Wolter, Michael Zakharyaschev
TL;DR
The paper investigates the interpolant existence problem for logics lacking Craig interpolation, specifically $\mathsf{wK4}$ and $\mathsf{DL}$. It proves that nonexistence of an interpolant can be certified by witnessing bisimilar descriptive models of polynomial size for $\mathsf{DL}$ and triple-exponential size for $\mathsf{wK4}$, placing the IEP in $coNP$ for $\mathsf{DL}$ and $coN3ExpTime$ for $\mathsf{wK4}$, with a matching $coNExpTime$-hardness bound for the latter. The $\mathsf{wK4}$ upper bound rests on a 3-exponential-size $\varrho$-bisimilarity-driven construction and a filtration-like reduction that preserves the absence of an interpolant, yielding a decision procedure in $coN3ExpTime$. The lower bound follows from a reduction from the exponential torus tiling problem, showing $coNExpTime$-hardness for $\mathsf{wK4}$. Together, the results delineate the complexity landscape of IEP for non-CIP modal logics and motivate further work on constructive interpolants and related definability problems.
Abstract
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.