一、自然推理系统 　　本节要介绍的是只含∧,,三个逻辑联结词的自然推理系统，由 Prawitz 创建。Prawitz 的自然推理系统是直觉主义逻辑的一部分，特点是逻辑对称性清楚、明确，从某个角度说是 Gentzen 的串形演算的起点；在机器上执行方便，同时真值在推理过程中的"传递"揭示得非常清楚。所以得到人工智能专家的重视。 　　注意到在证明论中，自然推理系统、Gentzen 串形演算、线性逻辑等系统中，主要的对象是证明过程而不是公理系统。特别要注意到的是，在语法上一个推理规则的一点点的增强或者减弱，或者一个规则的删除，都在本质上（语义上、哲学上）导致巨大的差异。这点是需要读者在学习和研究的实践中慢慢体会和理解的。 　　在该自然推理系统中，一个证明是一个类似于树形的图，可能有一个或者多个假设，或者没有假设，只含一个结论。 　　1．基本概念 　　我们将使用形为 　　　　　　　　 　　　　　　 A 　　的标记来代表一个自然推理的证明。这里A是推理的结论，是一个有穷树的根。该树的"树叶"一种是"有生命的"语句，一种是"无生命的"语句。 　　2．推理规则 　　（1）前提A 　　（2）导入规则 　　（3）消除规则 　　3．自然推理系统的可计算语义 　　将定义一些代数运算，与以上列出的规则一一对应，然后定义代数项。此框架下的代数运算完全与自然推理的证明过程"同构"，这就是著名的 " Curry-Howard 同构" 。 　　（1） 定义 　　（2） 举例，给出逻辑与代数计算的一一同构对应。 　　4．Curry - Howard 同构 　　已看到自然推理的推理（证明）与函数项之间的一一对应关系，对以下定义一个结构式形式的类型项的集合来说，将成为自然推理的所有推理的集合及这个项的集合之间的一个同构。这就是著名的 Curry - Howard 同构。