One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
Bulletin of the Section of Logic (2021)
- Volume: 50, Issue: 1, page 55-80
- ISSN: 0138-0680
Access Full Article
topAbstract
topHow to cite
topPaweł Płaczek. "One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity." Bulletin of the Section of Logic 50.1 (2021): 55-80. <http://eudml.org/doc/296788>.
@article{PawełPłaczek2021,
abstract = {Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.},
author = {Paweł Płaczek},
journal = {Bulletin of the Section of Logic},
keywords = {Substructural logic; Lambek calculus; nonassociative linear logic; sequent system; PTime complexity},
language = {eng},
number = {1},
pages = {55-80},
title = {One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity},
url = {http://eudml.org/doc/296788},
volume = {50},
year = {2021},
}
TY - JOUR
AU - Paweł Płaczek
TI - One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
JO - Bulletin of the Section of Logic
PY - 2021
VL - 50
IS - 1
SP - 55
EP - 80
AB - Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.
LA - eng
KW - Substructural logic; Lambek calculus; nonassociative linear logic; sequent system; PTime complexity
UR - http://eudml.org/doc/296788
ER -
References
top- [1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, The Journal of Symbolic Logic, vol. 56(4) (1991), pp. 1403–1451, DOI: http://dx.doi.org/10.2307/2275485
- [2] A. Bastenhof, Categorial Symmetry, Ph.D. thesis, Utrecht University (2013).
- [3] W. Buszkowski, On classical nonassociative Lambek calculus, [in:] M. Amblard, P. de Groote, S. Pogodalla, C. Retoré (eds.), Logical Aspects of Computational Linguistics, vol. 10054 of Lecture Notes in Computer Science, Springer (2016), pp. 68–84, DOI: http://dx.doi.org/10.1007/978-3-662-53826-5_5
- [4] W. Buszkowski, Involutive nonassociative Lambek calculus: Sequent systems and complexity, Bulletin of the Section of Logic, vol. 46(1/2) (2017), DOI: http://dx.doi.org/10.18778/0138-0680.46.1.2.07
- [5] P. De Groote, F. Lamarche, Classical non-associative Lambek calculus, Studia Logica, vol. 71(3) (2002), pp. 355–388, DOI: http://dx.doi.org/10.1023/A:1020520915016
- [6] N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the American Mathematical Society, vol. 365(3) (2013), pp. 1219–1249, URL: https://www.jstor.org/stable/23513444
- [7] N. Galatos, H. Ono, Cut elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic, vol. 161(9) (2010), pp. 1097–1133, DOI: http://dx.doi.org/0.1016/j.apal.2010.01.003
- [8] J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–101, DOI: http://dx.doi.org/10.1016/0304-3975(87)90045-4
- [9] J. Lambek, On the calculus of syntactic types, [in:] R. Jakobson (ed.), Structure of language and its mathematical aspects, vol. 12, Providence, RI: American Mathematical Society (1961), pp. 166–178, DOI: http://dx.doi.org/10.1090/psapm/012/9972
- [10] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae, vol. 22(1, 2) (1995), pp. 53–67, DOI: http://dx.doi.org/10.3233/FI-1995-22123
- [11] M. Pentus, Lambek calculus is NP-complete, Theoretical Computer Science, vol. 357(1-3) (2006), pp. 186–201, DOI: http://dx.doi.org/10.1016/j.tcs.2006.03.018Get.
NotesEmbed ?
topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.