Bunched logics displayed
Bunched logics are substructural logics with both \textit{multiplicative} (i.e., ``intensional) and \textit{additive} (i.e., ``extensional) logical connectives. These logics are important in computer science. The main four bunched logics are defined. Consider the four well-known elementary logics that follow: classical logic (CL), intuitionistic logic (IL), Lambek multiplicative logic (LM), and De Morgan multiplicative logic (dMM). Then, the four main bunched logics are the following: the logic of bunched implications (BI: IL+LM), Boolean BI (BBI: CL+LM), De Morgan BI (dmBI: IL+dMM), and classical BI (CBI: CL+dMM). Bunched logics have mostly been studied from a semantical point of view due to the computational significance of the resulting models. However, the present approach is proof-theoretical. In this sense, the author claims that the present paper is the ``first proof-theoretic treatment of bunched logic as a whole to appear in the literature (p. 1251). The proof-theoretical tools employed are the well-known display calculi introduced by Belnap. In particular, a unified display calculus proof-theory is defined for the main bunched logics mentioned above. The main results are the following. (a) The display calculi for each one of the four logics are proven to be sound and complete with respect to an appropriate sense of these notions (Section 3). (b) It is proved that cut is eliminable in each one of the calculi by demonstrating that they meet Belnap's cut-elimination conditions (Section 4). (c) It is shown how to limit exhaustive proof-searches to finitely branching ones (Section 4). Also, the following may be noted: (d) a classical deduction theorem for both the display calculi of BBI and CBI is proved (Section 5); (e) the relationship between display and sequent calculi for BI is investigated. Finally, in a closing section (Section 7), some suggestions concerning the application of the calculi defined are made.
- A unified display proof theory for bunched logic
- BI as an assertion language for mutable data structures
- Bunched polymorphism
- Classical BI
- Classical BI: Its Semantics and Proof Theory
- Constructive negation, implication, and co-implication
- Context logic as modal logic, completeness and parametric inexpressivity
- Decision problems for propositional linear logic
- Display logic
- Displaying and deciding substructural logics. I: Logics with contraposition
- Enhancing modular OO verification with separation logic
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- Expressivity Properties of Boolean BI Through Relational Models
- From IF to BI. A tale of dependence and separation
- Gaggles, Gentzen and Galois: how to display your favourite substructural logic
- scientific article; zbMATH DE number 970628 (Why is no real title available?)
- Logical Approaches to Computational Barriers
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Relational inductive shape analysis
- Strong update, disposal, and encapsulation in bunched typing
- The Logic of Bunched Implications
- The semantics and proof theory of the logic of bunched implications
- The semantics of BI and resource tableaux
- Undecidability of propositional separation logic and its neighbours
- Displaying modal logic
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Hypersequent and display calculi -- a unified perspective
- Bilattice logic properly displayed
- The semantics and proof theory of the logic of bunched implications
- Stone-type dualities for separation logics
- A unified display proof theory for bunched logic
- Undecidability of propositional separation logic and its neighbours
- The Logic of Bunched Implications
- Separation logics and modalities: a survey
- A labelled sequent calculus for BBI: proof theory and proof search
- Bunched hypersequent calculi for distributive substructural logics
- A complete axiomatisation for quantifier-free separation logic
- Power and limits of structural display rules
- Abstract hidden Markov models: a monadic account of quantitative information flow
- scientific article; zbMATH DE number 966898 (Why is no real title available?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Semantical analysis of the logic of bunched implications
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Universal proof theory: semi-analytic rules and Craig interpolation
- Inferentialist resource semantics
- Internal and external calculi: ordering the jungle without being lost in translations
This page was built for publication: Bunched logics displayed
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1935559)
