Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
arxiv(2024)
摘要
The interpolant existence problem (IEP) for a logic L is to decide, given
formulas P and Q, whether there exists a formula I, built from the shared
symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the
Craig interpolation property (CIP), then the IEP reduces to validity in L.
Recently, the IEP has been studied for logics without the CIP. The results
obtained so far indicate that even though the IEP can be computationally harder
than validity, it is decidable when L is decidable. Here, we give the first
examples of decidable fragments of first-order logic for which the IEP is
undecidable. Namely, we show that the IEP is undecidable for the two-variable
fragment with two equivalence relations and for the two-variable guarded
fragment with individual constants and two equivalence relations. We also
determine the corresponding decidable Boolean description logics for which the
IEP is undecidable.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要