Action Logic is Undecidable
| Autor: | Stepan L. Kuznetsov |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Discrete mathematics
General Computer Science Logic Distributivity 010102 general mathematics 0102 computer and information sciences 01 natural sciences Algebraic logic Theoretical Computer Science Undecidable problem Decidability Computational Mathematics Recursively enumerable language Action (philosophy) 010201 computation theory & mathematics Completeness (logic) Kleene star 0101 mathematics Mathematics |
| Zdroj: | ACM Transactions on Computational Logic. 22:1-26 |
| ISSN: | 1557-945X 1529-3785 |
| Popis: | Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. One of the operations of this logic is the Kleene star, which is axiomatized by an induction scheme. For a stronger system that uses an -rule instead (infinitary action logic), Buszkowski and Palka (2007) proved -completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by Kozen in 1994. In this article, we show that it is undecidable, more precisely, -complete. We also prove the same undecidability results for all recursively enumerable logics between action logic and infinitary action logic, for fragments of these logics with only one of the two lattice (additive) connectives, and for action logic extended with the law of distributivity. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|