Two results are presented concerning the entailment problem in Separation Logic with inductively defined predicate symbols and theory reasoning. First, we show that the entailment problem is undecidable for rules with bounded tree-width, if theory reasoning is considered. The result holds for a wide class of theories, even with a very low expressive power. For instance it applies to the natural numbers with the successor function, or with the usual order. Second, we show that every entailment problem can be reduced to an entailment problem containing no equality (neither in the formulas nor in the recursive rules defining the semantics of the predicate symbols).

翻译：首先,我们证明,如果考虑理论推理的话,对带条纹的树宽规则来说,产生的问题是不可估量的。结果支持着广泛的理论,即使表达力非常低。例如,它适用于具有后继功能或通常顺序的自然数字。第二,我们表明,每个产生问题都可以减少到一个不具有平等性的必然问题(无论是在公式中,还是在确定上游符号的语义的循环规则中)。