Subatomic Proof Systems
Subatomic Proof Systems
复制标题
亚原子证明系统
DOI：
10.1145/3173544
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Alessio Guglielmi
中科院分区：
文献类型：
--
作者：
Andrea Aler Tubella;Alessio Guglielmi
本文介绍了一系列结果中的第一篇，这些结果使我们能够开发出一种理论，可以更好地控制归一化的复杂性，特别是削减消除的复杂性。通过将原子视为自对偶非交换连接词，我们能够以统一且非常简单的方式对一大类推理规则进行分类。这使我们能够定义易于验证的简单条件，并通过一般定理确保标准化和削减消除。在本文中，我们定义并考虑了可分裂系统，它本质上构成了一大类线性逻辑，包括乘法线性逻辑和 BV，并且我们为它们证明了分裂定理，保证了割消除和其他可接纳结果作为推论。在接下来的文章中，我们将把这个结果扩展到非线性逻辑。最终结果将是一个综合理论，对大多数现有逻辑进行统一处理，并为未来证明系统的设计提供蓝图。
This article presents the first in a series of results that allow us to develop a theory providing finer control over the complexity of normalization, and in particular of cut elimination. By considering atoms as self-dual noncommutative connectives, we are able to classify a vast class of inference rules in a uniform and very simple way. This allows us to define simple conditions that are easily verifiable and that ensure normalization and cut elimination by way of a general theorem. In this article, we define and consider splittable systems, which essentially make up a large class of linear logics, including Multiplicative Linear Logic and BV, and we prove for them a splitting theorem, guaranteeing cut elimination and other admissibility results as corollaries. In articles to follow, we will extend this result to nonlinear logics. The final outcome will be a comprehensive theory giving a uniform treatment for most existing logics and providing a blueprint for the design of future proof systems.