Complexity tools for linear and substructural logics

Substructural logics are logical systems which lack all or some of the structural rules: contraction, weakening, commutativity, or even associativity. The tradition of linear logic, introduced by Girard for modelling resource-conscious reasoning, also fits into the substructural paradigm, as well as relevance logic, the Lambek calculus, and other systems. From the algorithmic point of view, substructural logics behave very differently: some of them are decidable and belong to relatively low complexity classes ($\mathsf{P}$, $\mathsf{NP}$, $\mathsf{PSPACE}$), some are undecidable ($\Sigma^0_1$-complete), and some are decidable, but non-elementary. Extending substructural logics with Kleene star, or more general fixed point operators, raises complexity even higher, up to $\Pi^1_1$-completeness. The lack of structural rules, however, makes the reductions and encodings used to prove complexity results quite complicated. In this talk, we give a survey of tools, methods, and tricks, which are used to establish complexity bounds for various linear and substructural logical systems.