A superposition calculus for separation logic

DOI10.1007/978-3-032-32592-1_3MaRDI QIDQ7411294zbMATH OpenFDO

Authors Tanguy Bozec, Nicolas Peltier

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32592-1_3

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A complete superposition calculus for primal grammars
• A comprehensive framework for saturation theorem proving
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• A decision procedure for satisfiability in separation logic with inductive predicates
• A fully syntactic AC-RPO.
• An efficient cyclic entailment procedure in a fragment of separation logic
• Automated cyclic entailment proofs in separation logic
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• BI as an assertion language for mutable data structures
• Compositional entailment checking for a fragment of separation logic
• Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
• Expressive completeness of separation logic with two variables and no separating conjunction
• Faster, higher, stronger: E 2.3
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 1765672 (Why is no real title available?)
• scientific article; zbMATH DE number 1765682 (Why is no real title available?)
• Induction in saturation
• Ordered chaining calculi for first-order theories of transitive relations
• Paramodulation-based theorem proving
• Positive deduction modulo regular theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Separation logic with one quantified variable
• Superposition for higher-order logic
• Superposition with datatypes and codatatypes
• Superposition with structural induction
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• The effects of adding reachability predicates in quantifier-free separation logic
• The tree width of separation logic with recursive definitions
• Verified heap theorem prover by paramodulation

This page was built for publication: A superposition calculus for separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411294)