非结合兰贝克演算加法扩展中判定问题的计算复杂性

我们分析了允许 sequent 前件为空的布尔非结合兰贝克演算 ($\mathsf{BFNL^*}$) 以及分配完全非结合兰贝克演算 ($\mathsf{DFNL}$) 推论关系的判定问题复杂性。我们构建了从模态逻辑 $\mathsf{K}$ 到 $\mathsf{BFNL^*}$ 的多项式归约。因此，我们证明了 $\mathsf{BFNL^*}$ 的判定问题是 PSPACE-hard 的。我们还通过将 $\mathsf{BFNL^*}$ 在多项式时间内归约到 enriched with 有限假设集的 $\mathsf{DFNL}$，证明了相同结果适用于 $\mathsf{DFNL}$ 的推论关系。最后，我们证明了 $\mathsf{BFNL^*}$ 变体的类似结果，包括 $\mathsf{BFNL^*e}$（带交换的 $\mathsf{BFNL^*}$），以及针对 $i \in \{\mathsf{K}, \mathsf{T}, \mathsf{K4}, \mathsf{S4}, \mathsf{S5}\}$ 的 $\mathsf{BFNL^*_i}$ 和 $\mathsf{BFNL^*_{ei}}$ 的模态扩展。