Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics

A. R. Balasubramanian*, Timo Lang, Revantha Ramanayake

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

1 Citaat (Scopus)
29 Downloads (Pure)


We establish decidability for the infinitely many
axiomatic extensions of the commutative Full Lambek logic with
weakening FLew (i.e. IMALLW) that have a cut-free hypersequent
proof calculus. Specifically: every analytic structural rule exten-
sion of HFLew. Decidability for the corresponding extensions of its
contraction counterpart FLec was established recently but their
computational complexity was left unanswered. In the second
part of this paper, we introduce just enough on length functions
for well-quasi-orderings and the fast-growing complexity classes
to obtain complexity upper bounds for both the weakening and
contraction extensions. A specific instance of this result yields
the first complexity bound for the prominent fuzzy logic MTL
(monoidal t-norm based logic) providing an answer to a long-
standing open problem.
Originele taal-2English
Titel2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Aantal pagina's13
StatusPublished - 7-jul-2021
Evenement36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 - Virtual, Online
Duur: 29-jun-20212-jul-2021


Conference36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
StadVirtual, Online

Citeer dit