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.

翻译：对于逻辑L，内插存在性问题（IEP）是指：给定公式P和Q，判断是否存在由P和Q的共享符号构造的公式I，使得在L中P蕴含I且I蕴含Q。若L具有克雷格内插性质（CIP），则IEP可归约为L中的有效性判定。近期，IEP已被研究用于不具备CIP的逻辑。目前所得结果表明，尽管IEP的计算复杂度可能高于有效性判定，但当L可判定时，IEP亦是可判定的。本文首次给出一阶逻辑可判定片段中IEP不可判定的实例。具体而言，我们证明：带有两个等价关系的二变量片段以及带有个体常元和两个等价关系的二变量受保护片段中，IEP是不可判定的。我们还确定了相应的可判定布尔描述逻辑中IEP不可判定的情形。