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规则更为简单。特别地，针对谓词由所谓loc-确定性归纳规则定义的特定片段，我们设计了一个在多项式时间内运行、可靠且完备的循环证明过程。本文还提供了若干复杂性下界，表明对给定条件的任何放宽都会导致问题变得不可判定。