A Proof Procedure for Separation Logic with Inductive Definitions and Data

A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoting structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2023-09, Vol.67 (3), p.30, Article 30
Main Authors: Echenim, Mnacho, Peltier, Nicolas
Format: Article
Language:English
Subjects:
Algorithms
Artificial Intelligence
Computer Science
Logic in Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Separation
Symbolic and Algebraic Manipulation
Trees
Validity
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoting structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that a sequent is valid iff it admits a (possibly infinite) proof tree. We also show that the procedure terminates in the two following cases: (i) When the inductive rules that define the predicates occurring on the left-hand side of the entailment terminate, in which case the proof tree is always finite. (ii) When the theory is empty, in which case every valid sequent admits a rational proof tree, where the total number of pairwise distinct sequents occurring in the proof tree is doubly exponential w.r.t. the size of the end-sequent.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-023-09680-4