A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoted structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that a sequent is valid iff it admits a (possibly infinite) proof tree. We show that the procedure terminates in the two following cases: (i) When the inductive rules that define the predicates occurring on the left-hand side of the entailment terminate, in which case the proof tree is always finite. (ii) When the theory is empty, in which case every valid sequent admits a rational proof tree, where the total number of pairwise distinct sequents occurring in the proof tree is doubly exponential w.r.t.\ the size of the end-sequent. We also show that the validity problem is undecidable for a wide class of theories, even with a very low expressive power.

翻译：以序列计算的精神, 提议了一个验证程序, 以检查分离逻辑公式( 分离逻辑公式, 结合自带定义的上游公式, 意指受约束树宽度和理论推理的结构) 的必然结果的有效性。 计算是健全和完整的, 意思是序列是有效的, 如果它承认了( 可能无限的) 证明树的话。 我们显示程序在以下两种情况下终止 : (一) 当给受约束木的左侧的上游下定义的暗示性规则, 而在这种情况下, 证明树始终是有限的。 (二) 当理论是空的, 每一个有效的序列都接受合理的证明树, 在这种情况下, 证明树上出现的对称不同序列的总数是双倍指数 w.r.t. \ 结束序列的大小。 我们还表明, 有效性问题对于广泛的理论来说是无法判断的, 即使是非常低的表达力 。