Bunched logics displayed
type: Item
instance of: scholarly article
title: Bunched logics displayed
zbMATH Open document ID: 1282.03011
author: James Brotherston
published in: Studia Logica
publication date: 2013-02-18T00:00:00Z
review text: 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.
reviewed by: Gemma Robles
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 6136997
zbMATH Keywords: bunched logic
zbMATH Keywords: display calculus
zbMATH Keywords: proof theory
zbMATH Keywords: cut elimination
describes a project that uses: jStar
MaRDI profile type: Publication
full work available at URL: s11225-012-9449-0
OpenAlex ID: W2032230034
cites work: From IF to BI. A tale of dependence and separation
cites work: Display logic
cites work: Strong update, disposal, and encapsulation in bunched typing
cites work: A Unified Display Proof Theory for Bunched Logic
cites work: Classical BI
cites work: Classical BI: Its Semantics and Proof Theory
cites work: Undecidability of Propositional Separation Logic and Its Neighbours
cites work: Logical Approaches to Computational Barriers
cites work: Context logic as modal logic
cites work: Relational inductive shape analysis
cites work: Enhancing modular OO verification with separation logic
cites work: Bunched polymorphism
cites work: Expressivity Properties of Boolean BI Through Relational Models
cites work: The semantics of BI and resource tableaux
cites work: Gaggles, Gentzen and Galois: how to display your favourite substructural logic
cites work: BI as an assertion language for mutable data structures
cites work: Q5688807
cites work: Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
cites work: Decision problems for propositional linear logic
cites work: The Logic of Bunched Implications
cites work: The semantics and proof theory of the logic of bunched implications
cites work: Possible worlds and resources: The semantics of \(\mathbf{BI}\)
cites work: Displaying and deciding substructural logics. I: Logics with contraposition
cites work: Constructive negation, implication, and co-implication
DOI: 10.1007/S11225-012-9449-0
description: scientific article; zbMATH DE number 6136997