Two Results on Separation Logic With Theory Reasoning
Mnacho Echenim, Nicolas Peltier

TL;DR
This paper proves that the entailment problem in Separation Logic with theory reasoning is undecidable for rules with bounded tree-width, but also shows it can be reduced to a form without equality, advancing understanding of its computational limits.
Contribution
It establishes undecidability of the entailment problem under certain conditions and provides a reduction to an equality-free form, broadening theoretical insights.
Findings
Entailment problem is undecidable for rules with bounded tree-width with theory reasoning.
Any entailment problem can be reduced to an equality-free form.
Results apply to theories like natural numbers with successor or order.
Abstract
Two results are presented concerning the entailment problem in Separation Logic with inductively defined predicate symbols and theory reasoning. First, we show that the entailment problem is undecidable for rules with bounded tree-width, if theory reasoning is considered. The result holds for a wide class of theories, even with a very low expressive power. For instance it applies to the natural numbers with the successor function, or with the usual order. Second, we show that every entailment problem can be reduced to an entailment problem containing no equality (neither in the formulas nor in the recursive rules defining the semantics of the predicate symbols).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic
