Modular tableaux calculi for separation theories

DOI10.1007/978-3-319-89366-2_24MaRDI QIDQ1653006zbMATH OpenOpenAlexFDO

Authors Simon Docherty, David Pym

Publication date 17 July 2018

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

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)