|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
On the Complexity of Reasoning in Kleene Algebra with Commutativity Conditionsстатья
- Автор: Kuznetsov Stepan L.
- Сборник: Theoretical Aspects of Computing – ICTAC 2023
- Серия: Lecture Notes in Computer Science
- Том: 14446
- Год издания: 2023
- Издательство: Springer Nature
- Местоположение издательства: Switzerland
- Первая страница: 83
- Последняя страница: 99
- DOI: 10.1007/978-3-031-47963-2_7
- Аннотация: Kleene algebras are one of the basic algebraic structures used in computer science, involving iteration, or Kleene star. An important subclass of Kleene algebras is formed by -continuous ones. In his 2002 paper, Dexter Kozen pinpointed complexity of various logical theories for Kleene algebras, both in the general and in the -continuous case. Those complexity results range from equational theories to Horn theories, or reasoning from hypotheses. In the middle, there are fragments of Horn theories, with restrictions on hypotheses. For the case when the hypotheses are commutativity conditions, i.e., commutation equations for designated pairs of atoms, however, Kozen mentioned the complexity result (\Pi^0_1-completeness) only for the -continuous case, while the general case remained an open question. This was the only gap in Kozen’s table of results, and the present paper fills this gap. Namely, we prove that reasoning from commutativity conditions on the class of all Kleene algebras is \Sigma^0_1-complete. In particular, this problem is undecidable.
- Добавил в систему: Кузнецов Степан Львович