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