|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ПсковГУ |
||
Non-associative, Non-commutative Multi-modal Linear Logicстатья
- Авторы: Blaisdell Eben, Kanovich Max, Kuznetsov Stepan L., Pimentel Elaine, Scedrov Andre
- Сборник: Automated Reasoning, 11th International Conference, IJCAR 2022
- Серия: Lecture Notes in Computer Science
- Том: 13385
- Год издания: 2022
- Издательство: Springer International Publishing AG
- Местоположение издательства: Cham, Switzerland
- Первая страница: 449
- Последняя страница: 467
- DOI: 10.1007/978-3-031-10769-6_27
- Аннотация: 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 (𝖺𝖼𝖫𝖫Σ) admits the (multi)cut rule, and we prove two undecidability results for fragments/variations of 𝖺𝖼𝖫𝖫Σ.
- Добавил в систему: Кузнецов Степан Львович