The interpolant existence problem for weak K4 and difference logic
arxiv(2024)
摘要
As well known, weak K4 and the difference logic DL do not enjoy the Craig
inter- polation 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要