One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

Paweł Płaczek

doi:10.18778/0138-0680.2020.25

One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

Paweł Płaczek

Source

Bulletin of the Section of Logic > 2021 > 50 > 1 > 55-80

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.

Identifiers

journal ISSN :	2449-836X , 0138-0680
DOI	10.18778/0138-0680.2020.25

Authors

Paweł Płaczek

Adam Mickiewicz University, Faculty of Mathematics and Computer Science Uniwersytetu Poznanskiego 4, 61-614 Poznan, Poland

Keywords

Substructural logic Lambek calculus nonassociative linear logic sequent system PTime complexity

Additional information

Publication languages: English

Data set: DML

Publisher

Wydawnictwo Uniwersytetu Łódzkiego

Fields of science

No field of science has been suggested yet.

Bibliography

[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

see all

article

Read online
Download
Add to read later
Add to collection
Add to followed
Share

Export to bibliography


Assign to other user
	×
Wrong email address

INFONA - science communication portal

One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity $("#expandableTitles").expandable();

Source

Abstract

Identifiers

Authors

User assignment

Assignment remove confirmation

You're going to remove this assignment. Are you sure?

Paweł Płaczek

Keywords

Additional information

Publisher

Fields of science

Fields of science

Bibliography

[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).

Share

Export to bibliography

Reporting an error / abuse

Sending the report failed

Accessibility options

One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity