Past attempts have been made to apply Girard's linear logic to Lafont's interaction nets by treating "symbois" as logical rules, however, failed to come to a signijicant explanation. In this paper, we try to model "symbols" as external axioms and use "tensor" to describe partition of auxiliary ports. We show that our solution leads to a very natural logical interpretation of the computation on interaction nets.

交互作用网是Lafont[1]于1990年在POPL会议上提出的一种程序设计语言，本文我们从证明和程序的关系出发，使用线性逻辑作为一中长跑 集成逻辑讨论交互作用网的理论性质，得到下述结论：·网上的结点辅助商品的划分可表示成相应类型的张量积；·网上的计算等价于线性矢列演算中Principal-Cut的消去；·对于任何一个交互作用网，如果存在一个线性矢列演算与之对应，则该网是简单的。

本文给出一个新的线性逻辑的证明网的定义并证明了所定义的证明网是线性逻辑的自然推理。和Girard的原定义相比，使用本文给出的定义来判定一个证明结构是否为证明网的时间复杂度为O（n*n），并且在证明所定义的证明网是可矢列化时更加自然和简单。

In 1986, J.Y. Girard discovered that usual logical implicaiton could be broken up into more clementary linear operations, Following that, he developed a new logical system, called linear logic, which appears now as a promising approach to fundamental questions arising in proof theory and in computer science, In this paper, we give a brief guide to the characteristics of linear logic, summary the recent developments and discuss the prospect of its applications to computer science.

Curry-Howard isomorphism has proved very fruitful as a methodological tool for exploiting the deep relationship among typed lambda calculus, intuitionistic logic and cartesian closed categories, A direct payoff of this has been the design of functional programming langages with powerful type systems, Limear logic is a logic of actions that seems weell suited for concurrent computation. In this paper, we establish a correspondence between Petri nets, linear logic and symmetic monoidal categories.