在Gentzen的串形演算中, 结构性规则包括弱减及收缩，简单地说，如果将这两条规则去掉，就导致了线性逻辑的建立。线性逻辑是在 1986 年左右，由法国逻辑学家 J.Y. Girard 创建的，被认为是证明论中的一个里程碑。在语法上的一个重要特征是该逻辑中的任一证明中的任一前提 A , 在证明中仅使用了一次。当然它还有许多逻辑上，或计算机科学理论上重要的特性，比如证明网络等。至今，人们已对线性逻辑作了大量的、深入的研究。 　　先介绍它的语义。可以说，线性逻辑的发现，是从对它的语义 --- 近邻空间--- 的研究中得到的。 一、近邻空间 　　定义8.4.1 一个近邻空间X是一个集合│X│，它的元素称为原子。 　　定义8.4.2 令X是一个近邻空间，X 的线性否定空间，记为 X┴ , 满足 　　（1）│X┴│ =│X│ 　　（2）x ︾ y [mod X┴] 当且仅当 x ︽y [mod X] 　　读者可以自行验证 X┴ ┴ = X 。 　　定义8.4.3 对任二近邻空间 X, Y ，以乘法连接词, ￡,分别定义由 X, Y 产生的一个新的近邻空间 Z , 这里│Z│=│X│×│Y│ 　　定义8.4.4 　　定义8.4.5 　　定义8.4.6