一个新的证明网定义及合理性

本文给出一个新的线性逻辑的证明网的定义并证明了所定义的证明网是线性逻辑的自然推理．和Ｇｉｒａｒｄ的原定义相比，使用本文给出的定义来判定一个证明结构是否为证明网的时间复杂度为Ｏ（ｎ＊ｎ），并且在证明所定义的证明网是可矢列化时更加自然和简单．

交互作用网理论分析

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