一句话：提出强分离逻辑，通过限制分离合取的语义，在保留魔法棒和归纳谓词的同时恢复可判定性。
大多数分离逻辑自动验证器基于符号堆片段，该片段不支持魔法棒算子，也不允许经典布尔算子作用于空间公式。这是因为支持魔法棒很快会导致不可判定性，尤其当与用于推理数据结构的归纳谓词结合时。为规避这些不可判定性结果，我们提出为分离合取赋予一种更严格的语义，由此得到强分离逻辑。我们论证，该逻辑可以像标准分离逻辑一样用于符号执行和溯因推理，同时在同时存在魔法棒和归纳谓词（我们考虑列表段谓词和树谓词）时仍保持可判定性——而这一特征组合在标准语义下会导致不可判定性。
Most automated verifiers for separation logic are based on the symbolic-heap fragment, which disallows both the magic-wand operator and the application of classical Boolean operators to spatial formulas. This is not surprising, as support for the magic wand quickly leads to undecidability, especially when combined with inductive predicates for reasoning about data structures. To circumvent these undecidability results, we propose assigning a more restrictive semantics to the separating conjunction. We argue that the resulting logic, strong-separation logic, can be used for symbolic execution and abductive reasoning just like “standard” separation logic, while remaining decidable even in the presence of both the magic wand and inductive predicates (we consider a list-segment predicate and a tree predicate)—a combination of features that leads to undecidability for the standard semantics.