Bunched logics displayed. (English) Zbl 1282.03011
Bunched logics are substructural logics with both multiplicative (i.e., “intensional”) and 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.
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.
Reviewer: Gemma Robles (León)
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03F05 | Cut-elimination and normal-form theorems |
Software:
jStarReferences:
| [1] | Abramsky , Samson , Jouko Väänänen: From IF to BI; a tale of dependence and separation. Synthese 167(2), 207–230 (2009) · Zbl 1175.03016 · doi:10.1007/s11229-008-9415-6 |
| [2] | Belnap, Jr., Nuel D., Display logic, Journal of Philosophical Logic 11:375–417, 1982. · Zbl 0509.03008 |
| [3] | Berdine, Josh, and Peter O’Hearn, Strong update, disposal and encapsulation in bunched typing, in Proceedings of MFPS-22, vol. 158 of ENTCS, Elsevier B.V., 2006, pp. 81–98. · Zbl 1273.03097 |
| [4] | Brotherston, James, A unified display proof theory for bunched logic, in Proceedings of MFPS-26, vol. 265 of ENTCS, Elsevier B.V., 2010, pp. 197–211. · Zbl 1343.03018 |
| [5] | Brotherston, James, and Cristiano Calcagno, Classical BI (A logic for reasoning about dualising resource), in Proceedings of POPL-36, ACM, 2009, pp. 328–339. · Zbl 1315.68175 |
| [6] | Brotherston, James, and Cristiano Calcagno, Classical BI: Its semantics and proof theory, Logical Methods in Computer Science 6:3, 2010. · Zbl 1198.03028 |
| [7] | Brotherston, James, and Max Kanovich, Undecidability of propositional separation logic and its neighbours, in Proceedings of LICS-25, IEEE Computer Society, 2010, pp. 137–146. · Zbl 1295.68166 |
| [8] | Brünnler, Kai, Deep inference and its normal form of derivations, in Proceedings of CiE, vol. 3988 of LNCS, 2006, pp. 65–74. · Zbl 1145.03333 |
| [9] | Calcagno, Cristiano, Philippa Gardner, and Uri Zarfaty, Context logic as modal logic: Completeness and parametric inexpressivity, in Proceedings of POPL- 34, ACM, 2007, pp. 123–134. · Zbl 1295.68079 |
| [10] | Chang, Bor-Yuh Evan, and Xavier Rival, Relational inductive shape analysis, in Proceedings of POPL-35, ACM, 2008, pp. 247–260. · Zbl 1295.68081 |
| [11] | Chin, Wei-Ngan, Cristina David, Huu Hai Nguyen, and Shengchao Qin, Enhancing modular OO verification with separation logic, in Proceedings of POPL-35, ACM, 2008, pp. 87–99. · Zbl 1295.68082 |
| [12] | Collinson , Matthew , David Pym, Edmund Robinson: Bunched polymorphism. Mathematical Structures in Computer Science 18(6), 1091–1132 (2008) · Zbl 1167.03011 · doi:10.1017/S0960129508007159 |
| [13] | Distefano, Dino, and Matthew Parkinson, jStar: Towards practical verification for Java, in Proceedings of OOPSLA, ACM, 2008, pp. 213–226. |
| [14] | Galmiche, Didier, and Dominique Larchey-Wendling, Expressivity properties of Boolean BI through relational models, in Proceedings of FSTTCS, vol. 4337 of LNCS, Springer, 2006, pp. 357–368. · Zbl 1168.03326 |
| [15] | Galmiche , Didier , Daniel Méry, David Pym: The semantics of BI and resource tableaux. Mathematical Structures in Computer Science 15, 1033–1088 (2005) · Zbl 1145.03308 · doi:10.1017/S0960129505004858 |
| [16] | Goré, Rajeev, Gaggles, Gentzen and Galois: How to display your favourite substructural logic, Logic Journal of the IGPL 6(5):669–694, 1998. · Zbl 0917.03025 |
| [17] | Ishtiaq, Samin, and Peter W. O’Hearn, BI as an assertion language for mutable data structures, in Proceedings of POPL-28, ACM, 2001, pp. 14–26. · Zbl 1323.68077 |
| [18] | Kracht, Marcus, Power and weakness of the modal display calculus, in Heinrich Wansing, (ed.), Proof Theory of Modal Logic, Kluwer, 1996, pp. 93–121. · Zbl 0864.03014 |
| [19] | Larchey-Wendling , Dominique , Didier Galmiche: Exploring the relation between intuitionistic BI and Boolean BI: An unexpected embedding. Mathematical Structures in Computer Science 19, 1–66 (2009) · Zbl 1169.03024 · doi:10.1017/S0960129509007567 |
| [20] | Larchey-Wendling, Dominique, and Didier Galmiche, The undecidability of Boolean BI through phase semantics, in Proceedings of LICS-25, IEEE Computer Society, 2010, pp. 140–149. · Zbl 1168.03326 |
| [21] | Lincoln , Patrick , John C. Mitchell, Andre Scedrov, Natarajan Shankar: Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56(1–3), 239–311 (1992) · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B |
| [22] | O’Hearn , Peter W., David J. Pym: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999) · Zbl 0930.03095 · doi:10.2307/421090 |
| [23] | Pym, David, The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series, Kluwer, 2002. Errata and remarks (Pym 2008) maintained at http://www.abdn.ac.uk/\(\sim\)csc335/BI-monograph-errata.pdf . · Zbl 1068.03001 |
| [24] | Pym , David , Peter O’Hearn, Hongseok Yang: Possible worlds and resources: The semantics of BI. Theoretical Computer Science 315(1), 257–305 (2004) · Zbl 1055.03021 · doi:10.1016/j.tcs.2003.11.020 |
| [25] | Read, Stephen, Relevant Logic: A Philosophical Examination, Basil Blackwell, 1987. |
| [26] | Reed, Jason, A Hybrid Logical Framework, Ph.D. thesis, Carnegie Mellon University, 2009. |
| [27] | Restall, Greg, Displaying and deciding substructural logics 1: Logics with contraposition, Journal of Philosophical Logic 27:179–216, 1998. · Zbl 0913.03029 |
| [28] | Reynolds, John C., Separation logic: A logic for shared mutable data structures, in Proceedings of LICS-17, IEEE Computer Society, 2002, pp. 55–74. |
| [29] | Wansing, Heinrich, Constructive negation, implication, and co-implication, Journal of Applied Non-Classical Logics 18(2–3):341–364 (2008) · Zbl 1181.03027 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
