A system of interaction and structure
A system of interaction and structure
复制标题
相互作用和结构的系统
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Alessio Guglielmi
中科院分区：
文献类型：
--
作者：
Alessio Guglielmi
本文介绍了一个称为 BV 的逻辑系统，它通过非交换自对偶逻辑运算符扩展了乘法线性逻辑。这种扩展对于后续微积分来说尤其具有挑战性，到目前为止还没有实现。在一种称为结构演算的新形式主义中，它变得非常自然，这是这项工作的主要贡献。结构是服从某些序列典型方程定律的公式。结构演算是通过推广序列演算来获得的，这种方式可以观察到新的自上而下的推导对称性，并且它采用在任何深度重写内部结构的推理规则。这些属性除了允许 BV 设计之外，还产生了模块化的切割消除证明。
This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulas subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalizing the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.