Tight complexity bounds for substructural logics

Abstract: Substructural logics constitute generalizations of classical and intuitionistic logic that allow for resource sensitive reasoning; they connect to philosophy, computer science, engineering, mathematical linguistics and theoretical physics. Their algebraic semantics, residuated lattices, have their independent history and relate to ring theory, lattice-ordered groups and Tarski’s relation algebras, among other algebraic structures.

We discuss the complexity of provability and of deduciblity of various substructural logics, ranging from low complexity classes to undecidability. Of particular interest are certain knotted extensions which have (non-elementary) complexity in the Ackermann level of the fast-growing hierarchy. We obtain lower complexity bounds by encoding suitable and-branching counter machines into the corresponding algebraic semantics, using the method of residuated frames. For the upper bounds, we undertake a proof-theoretic investigation of auxiliary analytic calculi and employ methods from the theory of well-ordered sets to obtain length theorems. Together, these yield tight complexity bounds for the logics under investigation. Our results cover both sequent and hypersequent calculi.

computational complexitylogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic