We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on the inductive rules that define the semantics of the predicates. We focus on so-called P-rules, which are similar to (but simpler than) the PCE rules introduced by Iosif et al. in 2013. In particular, for a specific fragment where predicates are defined by so-called loc-deterministic inductive rules, we devise a sound and complete cyclic proof procedure running in polynomial time. Several complexity lower bounds are provided, showing that any relaxing of the provided conditions makes the problem intractable.

翻译：我们针对分离逻辑中由用户自定义谓词表示递归数据结构的公式之间的蕴涵问题，建立了多种复杂度结果。所考虑的子片段通过定义谓词语义的归纳规则上的句法条件进行刻画。我们重点关注所谓的P-规则，该规则与Iosif等人于2013年提出的PCE规则相似但更简化。特别地，针对由所谓位置确定性归纳规则定义谓词的特定子片段，我们设计了一个可在多项式时间内运行的正确完备循环证明过程。此外，我们还给出了多个复杂度下界，表明任何对给定条件的放松都会使该问题变得不可处理。