一句话：证明了具有无割超序列演算的所有 HFLew 解析结构规则扩张可判定，并给出弱化与收缩扩张的复杂度上界及 MTL 的首个复杂度界。
本文研究交换 Full Lambek 逻辑带弱化 FLew（即 IMALLW）的无穷多公理扩张的可判定性与复杂度。作者证明：HFLew 的每个解析结构规则扩张都可判定，从而覆盖所有具有无割超序列证明演算的扩张；其收缩对应物 FLec 的相应扩张虽已知可判定，但复杂度此前未知。为此，文章引入面向良拟序的长度函数与快速增长复杂度类工具，为弱化和收缩两类扩张给出复杂度上界。作为一个具体实例，该结果首次给出著名模糊逻辑 MTL 的复杂度界，解决了长期开放问题。
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 extension 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 longstanding open problem.
@inproceedings{paperbot6194,
title = {Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics},
author = {A. R. Balasubramanian and Timo Lang and Revantha Ramanayake},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470733}
}