Temel Kavramlar
Deciding the existence of interpolants in weak K4 and difference logic.
Özet
The article discusses the problem of determining if a given implication has an interpolant in weak K4 and difference logic. It shows that nonexistence of an interpolant can be witnessed by bisimilar models of polynomial size for DL and triple-exponential size for weak K4. The interpolant existence problems for these logics are decidable in coNP and coN3ExpTime, respectively. The article also establishes the complexity of this problem for weak K4 as coNExpTime-hard. It delves into the modal logic weak K4 obtained from propositional classical modal language interpreted by derivative operation 1 in topological spaces. Additionally, it introduces the difference logic DL characterized by difference frames. Despite similarities to other logics, wK4 and DL lack the Craig interpolation property (CIP). Examples illustrate how certain formulas do not have interpolants in these logics due to bisimulations preserving truth-values. The paper provides technical tools and results for deciding the interpolant existence problem for both logics.
İstatistikler
Nonexistence of an interpolant can be witnessed by bisimilar models of polynomial size for DL.
Nonexistence of an interpolant can be witnessed by bisimilar models of triple-exponential size for weak K4.
Interpolant existence problems are decidable in coNP and coN3ExpTime.
Complexity is established as coNExpTime-hard for weak K4.