线性逻辑框架下的削减消除准则：扩展到更多逻辑系统

"这篇论文探讨了在线获取的线性逻辑（Linear Logic，LL）在证明系统中的应用，特别是在削减消除准则方面。研究由北里奥格兰德联邦大学的学者进行，他们使用线性嵌套证明（Linear Nested Sequent，LNS）系统，扩展了线性逻辑作为逻辑框架的能力，以支持更多逻辑系统的削减消除。" 线性逻辑是一种逻辑系统，其核心特征在于对量词的限制，强调资源的使用和管理。在传统逻辑中，量词（如全称量词和存在量词）允许无限复制和丢弃信息，而线性逻辑则不允许这样的操作，更注重信息的线性使用。削减消除准则是证明系统中的一个重要概念，它允许中间步骤的简化，使得证明更加直接且紧凑。在经典逻辑系统（如LK）和直觉逻辑系统（如LJ）中，已经证明了削减消除的充分条件。 在本文中，研究者们使用线性嵌套证明系统（LNS）来处理线性逻辑的一个变种——SLL（单重线性逻辑），并展示了如何在更广泛的逻辑系统类别中建立削减消除准则，包括K、K4、KT、KD和S4等模态逻辑系统，以及直觉逻辑的多结论LNS系统（mLJ）。LNS提供了一种有效的方法来编码不同逻辑系统，并利用SLL的元理论来建立这些编码的基本元属性。 论文强调，使用LNS形式主义的重要性在于它允许简洁地将对象逻辑（OL）编码到SLL中，同时利用SLL的元理论来验证OL的属性。这种编码方法不仅简化了逻辑系统的削减消除过程，还为自动化证明工具提供了基础，以避免在手动证明过程中可能出现的错误。 关键词涵盖了线性逻辑的核心概念——削减消除法，这是逻辑系统中证明构造的重要部分。削减消除在哲学、数学和计算机科学中具有广泛的应用，例如在类型理论、编程语言理论和自动证明系统中。 这篇论文发表于《理论计算机科学电子笔记》（Electronic Notes in Theoretical Computer Science），可以通过www.sciencedirect.com在线获取。该研究工作对于理解线性逻辑在证明理论中的作用，以及如何扩展其应用于更多逻辑系统，具有重要意义。通过这种方式，研究者们为逻辑框架的理论和实践提供了新的见解，促进了相关领域的研究进展。