|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
A logical framework with commutative and non-commutative subexponentialsстатья
Информация о цитировании статьи получена из
Scopus
Дата последнего поиска статьи во внешних источниках: 5 декабря 2018 г.
- Авторы: Kanovich Max, Kuznetsov Stepan, Nigam Vivek, Scedrov Andre
- Сборник: Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
- Серия: Lecture Notes in Artificial Intelligence
- Том: 10900
- Год издания: 2018
- Место издания: Springer
- Первая страница: 228
- Последняя страница: 245
- DOI: 10.1007/978-3-319-94205-6_16
- Аннотация: Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic frameworks by allowing the distinction of multiple contexts. These contexts may behave as multisets of formulas or sets of formulas. Motivated by applications in distributed systems and in type-logical grammar, we propose a linear logical framework containing both commutative and non-commutative subexponentials. Non-commutative subexponentials can be used to specify contexts which behave as lists, not multisets, of formulas. In addition, motivated by our applications in type-logical grammar, where the weakenening rule is disallowed, we investigate the proof theory of formulas that can only contract, but not weaken. In fact, our contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.
- Добавил в систему: Кузнецов Степан Львович