A Local System for Linear Logic
A Local System for Linear Logic
复制标题
线性逻辑的局部系统
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Lutz Straßburger
中科院分区：
文献类型：
--
作者：
Lutz Straßburger
在本文中，我将给出一个线性逻辑的演绎系统，其中所有的规则都是局部的。特别是，收缩规则被简化为原子版本，并且不存在全局提升规则。为了达到这一目的，有必要从序列演算出发，使用结构演算，它是片面的顺序演算的推广。在规则中，前提和结论不是顺序，而是结构，它们是共享公式和顺序性质的表达式。
In this paper I will present a deductive system for linear logic, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. In order to achieve this, it is necessary to depart from the sequent calculus and use the calculus of structures, which is a generalization of the one-sided sequent calculus. In a rule, premise and conclusion are not sequents, but structures, which are expressions that share properties of formulae and sequents.