线性逻辑的新削减消除准则：拓展到SLL和更多系统

本文探讨了线性逻辑中的新视角及其削减消除准则在理论计算机科学中的应用。线性逻辑，作为一种强大的逻辑框架，以其独特的分析性质而闻名，即解析性，它确保证明过程中只使用公式本身的子句。解析性通常通过证明割消规则的可容许性来实现，即无需外部引理，可以直接从已知前提推导出结论。这种技术在证明系统中具有重要意义，因为它简化了证明过程，减少了错误发生的可能性，并且在实践中常常依赖于半自动或自动化的证明转换工具。 先前的研究者如Miller和Pimentel利用线性逻辑（LL）作为逻辑框架，已经成功地为一些逻辑系统建立了对象逻辑割消的充分条件，包括LK（经典逻辑）、LJ（直觉逻辑）和MALL（子结构逻辑）等。然而，这些工作并未涵盖所有逻辑系统，尤其是那些不能完全编码在LL中的系统，如模态逻辑的可重构系统，因为它们涉及到更复杂的结构和语义。 本文的创新之处在于引入了线性嵌套证明（LNS）表示的SLL（一种扩展的线性逻辑），并展示了如何用这种方法扩展削减消除准则的应用范围，涵盖了LNS证明系统的K、KT、KD、S4以及多结论LNS版本的直觉逻辑（mLJ）。值得注意的是，尽管处理了更为复杂的形式系统，但提出的割消充分条件仍然保持着与Miller和Pimentel工作的简洁性。 关键在于选择合适的理论基础，作者采用了基于LNS的对象逻辑系统，这不仅提供了对OL到SLL的直观编码，而且使得利用SLL的元理论来探讨基本元属性成为可能。这种成果对于哲学、数学和计算机科学领域的逻辑系统验证，特别是那些涉及自动验证和削减消除的系统，具有重要的实践价值。 文章发表在《理论计算机科学电子笔记》上，可以通过Elsevier的网站获取，遵循CCBY-NC-ND许可证的开放获取政策，便于学术界和研究者共享和讨论这一新的理论进展。