Complexity of Substructural Logics with Kleene Star
Steklov Mathematical Institute of RAS
Abstract:
The multiplicative-additive Lambek calculus (a basic substructural logic) extended with iteration modality (Kleene star) axiomatises the inequational theory of residuated Kleene lattices, that is, Kleene algebras extended with meet and residuals. If one additionally adds the exponential modality, the system becomes capable of encoding more complicated theories, like the Horn one, for this class of algebraic structures. In this talk we survey algorithmic complexity results of substructural logics with Kleene star (both non-commutative and commutative), including results recently obtained by the author.