论文标题
与理论推理有关分离逻辑的两个结果
Two Results on Separation Logic With Theory Reasoning
论文作者
论文摘要
与归纳定义的谓词符号和理论推理有关分离逻辑中的累积问题，给出了两个结果。首先，我们表明，如果考虑理论推理，则需要对具有有限树宽度的规则确定。结果也适用于广泛的理论，即使具有非常低的表达能力。例如，它适用于带有后继函数或通常顺序的自然数。其次，我们表明，每个需要问题都可以简化为不包含平等的需要问题（在公式中也不是在定义谓词符号语义的递归规则中）。
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).
