Hypersequent Calculi Have Ackermannian Complexity

A. R. Balasubramanian, Vitor Greati, Revantha Ramanayake

For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on ${\mathbb{N}}^d$ (Dickson's lemma), yi…