Abstract This paper presents a novel extension of the superposition calculus for reasoning about formulas in Separation Logic (SL). Our approach integrates the efficiency of saturation-based theorem proving with the expressive power of SL, which is widely used to describe and reason about memory heaps. The target logic strictly extends first-order equational logic with SL constructs built from points-to atoms and separating conjunctions. The resulting calculus retains the core strengths of the superposition paradigm while addressing the distinctive semantic challenges of SL. We prove that the calculus is sound and complete w.r.t the standard redundancy criterion.

Abstract The predicate definitions in Separation Logic (SL) play an important role: they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. [8] proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly nonterminating) algorithm to transform arbitrary ID into equivalent PCE definitions when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable. The algorithm has been implemented, and experimental results are reported on a benchmark, including significant examples from .