1．规则 　　一个串形是形为A!│-B!的一个表达式。这里A! ,B!分别是公式的有穷序列A1,A2,…,An 及B1,B2,…,Bm。该表达式的直觉解释为由A1∧A2∧…∧An 可推出析取式B1∧B2∧…∧Bm 。特别是 　　a 如果A! 是空集，则B1∨B2∨…∨Bm是一个可证公式。 　　b 如果A! 是空集，而B! 只含一个公式B, 则B可证。 　　c 若B! 是空集，则A1∧A2∧…∧An的否定可证。 　　d 若A! 及B! 都是空集，则意味着矛盾出现。 　　（1） 恒等式 　　a．对任意公式 C , C│- C 称为恒等公理。 　　b．Cut 规则 　　　 　　（2）结构性规则 　　a．变位规则 　　　 　　b．弱减规则 　　　 　　c．收缩规则 　　　 　　对这些规则的重要性，人们几乎是近年来才发现。可以说，线性逻辑是对这些结构性规则的修改和删除才建立起来的。 　　（3）逻辑规则 　　a．否定规则 　　　 　　b．合取规则 　　　 　　　　 　　c．析取规则 　　　 　　　　 　　d．蕴涵规则 　　　 　　e． 全称量词规则 　　　 　　在R规则中，a 在A!,B!中没有自由出现。 　　f．存在量词规则 　　　 　　在 L规则中，a 在A!,B! 中没有自由出现。 　　这里有几点我们需要说明一下： 　　（1） Gentzen 的串形演算系统与任何形式的经典谓词演算系统是等价的。它的特点是表达自然，所以有时人们也称它或者它的某种变形"自然推理系统"。但这一类串形推理系统与8.3.1介绍的自然推理系统是不同的。 　　（2） 串形演算有很好的对称性，或者说，它将逻辑的对称性描叙得很清楚。读者比较各组规则即可以发现这一点。 　　（3） 在 8.3.1 中介绍了自然推理系统的 Curry - Howard 对应。同时也可以将自然推理系统对应到串形演算的某一部分中。或者反过来说，串形演算的某一部分,与8.3.1 中的自然推理系统同构。由 Curry - Howard 同构, 自然推理系统中的每一个证明与一个带类型的λ-项对应。由 Church -Rosser 定理，每一个λ- 项，如果有范式，则范式是唯一的。又由 Curry - Howard 同构，自然推理系统的正规化是说每一个自然推理系统的一个证明都等价于一个不带"已失效"的前提的证明。这就是著名的自然推理系统中的 Normalization 定理 。 　　（4） 由 (3) , 既然自然推理系统是串形演算的一部分，自然推理系统的 normalization 能以什么样的形式扩充到串形演算中呢？这就是著名的 " Hauptsatz", 也称 " Cut Elimination " ，陈述出来，就是著名的 Gentzen 定理: 在串形演算中，对每一个证明π, 都存在与π等价的一个证明π' ,π'中未使用 cut 规则。