A non-uniform view of Craig interpolation in modal logics with linear frames
CoRR(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要