论文标题
命题非缔合线性逻辑和扩展的决策问题
Decision Problems for Propositional Non-associative Linear Logic and Extensions
论文作者
论文摘要
在我们以前的工作中，我们提出了通过添加一种线性逻辑模态从完整的非相关Lambek微积分获得的逻辑。我们称此逻辑非缔合性非共同直觉线性逻辑（简称为$ \ mathbf {nacill} $）。在本文中，我们为$ \ mathbf {nacill} $的各种扩展范围建立了可定义性和不确定性结果。关于可确定性结果，我们表明，左旋规则可以决定$ \ mathbf {nacill} $的几个扩展问题的可推迟性问题。关于不可证明的结果，我们表明，通过收缩和交换规则，非缔合性非交往的经典线性逻辑的所有扩展是不可决定的。
In our previous work, we proposed the logic obtained from full non-associative Lambek calculus by adding a sort of linear-logical modality. We call this logic non-associative non-commutative intuitionistic linear logic ($\mathbf{NACILL}$, for short). In this paper, we establish the decidability and undecidability results for various extensions of $\mathbf{NACILL}$. Regarding the decidability results, we show that the deducibility problems for several extensions of $\mathbf{NACILL}$ with the rule of left-weakening are decidable. Regarding the undecidability results, we show that the provability problems for all the extensions of non-associative non-commutative classical linear logic by the rules of contraction and exchange are undecidable.
