|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
The Lambek calculus with iteration: two variantsстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Дата последнего поиска статьи во внешних источниках: 2 мая 2018 г.
- Автор: Stepan Kuznetsov
- Сборник: Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings
- Серия: Lecture Notes in Computer Science
- Том: 10388
- Год издания: 2017
- Место издания: Springer
- Первая страница: 182
- Последняя страница: 198
- DOI: 10.1007/978-3-662-55386-2_13
- Аннотация: Formulae of the Lambek calculus are constructed using three binary connectives, multiplication and two divisions. We extend it using a unary connective, positive Kleene iteration. For this new operation, following its natural interpretation, we present two lines of calculi. The first one is a fragment of infinitary action logic and includes an omega-rule for introducing iteration to the antecedent. We also consider a version with infinite (but finitely branching) derivations and prove equivalence of these two versions. In Kleene algebras, this line of calculi corresponds to the *-continuous case. For the second line, we restrict our infinite derivations to cyclic (regular) ones. We show that this system is equivalent to a variant of action logic that corresponds to general residuated Kleene algebras, not necessarily *-continuous. Finally, we show that, in contrast with the case without division operations (considered by Kozen), the first system is strictly stronger than the second one. To prove this, we use a complexity argument. Namely, we show, using methods of Buszkowski and Palka, that the first system is \(\varPi _1^0\) -hard, and therefore is not recursively enumerable and cannot be described by a calculus with finite derivations.
- Добавил в систему: Кузнецов Степан Львович