Blaisdell, E;
Kanovich, M;
Kuznetsov, SL;
Pimentel, E;
Scedrov, A;
(2022)
Non-associative, Non-commutative Multi-modal Linear Logic.
In: Blanchette, J and Kovács, L and Pattinson, D, (eds.)
Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings.
(pp. pp. 449-467).
Springer: Cham, Switzerland.
Preview |
Text
978-3-031-10769-6_27.pdf - Published Version Download (460kB) | Preview |
Abstract
Adding multi-modalities (called subexponentials) to linear logic enhances its power as a logical framework, which has been extensively used in the specification of e.g. proof systems, programming languages and bigraphs. Initially, subexponentials allowed for classical, linear, affine or relevant behaviors. Recently, this framework was enhanced so to allow for commutativity as well. In this work, we close the cycle by considering associativity. We show that the resulting system (acLLΣ ) admits the (multi)cut rule, and we prove two undecidability results for fragments/variations of acLLΣ.
| Type: | Proceedings paper |
|---|---|
| Title: | Non-associative, Non-commutative Multi-modal Linear Logic |
| Event: | IJCAR 2022: 11th International Joint Conference on Automated Reasoning |
| ISBN-13: | 978-3-031-10768-9 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-031-10769-6_27 |
| Publisher version: | https://doi.org/10.1007/978-3-031-10769-6_27 |
| Language: | English |
| Additional information: | This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10154867 |
Archive Staff Only
 |
View Item |
