Modular tableaux calculi for separation theories

DOI10.1007/978-3-319-89366-2_24zbMATH Open1506.03073OpenAlexW2788044110MaRDI QIDQ1653006FDOQ1653006

Authors: Simon Docherty, David Pym 

Publication date: 17 July 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-89366-2_24

Recommendations

• Tableaux and resource graphs for separation logic
• Modular labelled sequent calculi for abstract separation logics
• Proof search for propositional abstract separation logics via labelled sequents
• Parametric completeness for separation theories
• Program Verification with Separation Logic

zbMATH Keywords

proof theorysubstructural logicKripke semanticsseparation logictableauxbunched logiccoherent logicseparation theories

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70)

Cited In (9)

• Stone-type dualities for separation logics
• A complete axiomatisation for quantifier-free separation logic
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Modular labelled sequent calculi for abstract separation logics
• Semantical analysis of the logic of bunched implications
• Parametric completeness for separation theories
• Proof search for propositional abstract separation logics via labelled sequents
• Tableaux and resource graphs for separation logic
• Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles

This page was built for publication: Modular tableaux calculi for separation theories

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