二、Gentzen 串形演算 　　Gentzen 关于一阶逻辑的串形演算被认为是对逻辑的对称性的最漂亮的刻画。事实上，Prolog 语言是串形演算的一个子演算演变而来。同时，在自动定理证明中的"表格法"也是源出于串形演算。 　　但是从算法的角度来看，一般的串形演算并没有 Curry - Howard 对应。这是因为在一般串形演算中，同一个证明可以有多种方法写出来。自然推理系统当然是它的一个子系统，直觉主义逻辑也是它的一个子系统。在 Gentzen 的系统中，找到一个带多个结论的自然推理系统以其来描叙并行计算，是一个很有意义的探索方向。 　　1．规则 　　（1）恒等式 　　（2）结构性规则 　　（3）逻辑规则 　　2．直觉主义的串形演算 　　直觉主义逻辑，或者构造性逻辑，其本质是不接受排中律，或者矛盾律：对任何一个断言A, 或者A为真，或者A为真，别无其他选择。但在现实世界中，一个断言，比如，"这块木板是绿色的"，就有多种可能性。在这个例子中，原因在于不可能对"绿色"这个概念一个明确的界限。在语义上说，假定U是一个模型，任给一个公式A(x) , x 是唯一的自由变元，任给U中的一个元素 c, 经典逻辑认为，或者A( c ) 为真，或者A( c ) 为真。但实际上，有些元素 c , 我们目前或者永远不知道A( c ) 为真还是为假。