Mnacho Echenim ; Nicolas Peltier - Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates

fi:11318 - Fundamenta Informaticae, July 16, 2025, Volume 194, Issue 1 - https://doi.org/10.46298/fi.11318
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined PredicatesArticle

Authors: Mnacho Echenim ; Nicolas Peltier

    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.


    Volume: Volume 194, Issue 1
    Published on: July 16, 2025
    Accepted on: January 15, 2025
    Submitted on: May 16, 2023
    Keywords: Logic in Computer Science,68T27,I.2.3; F.4.1

    Consultation statistics

    This page has been seen 3 times.
    This article's PDF has been downloaded 2 times.