一、自然推理系统

  本节要介绍的是只含∧,,三个逻辑联结词的自然推理系统,由 Prawitz 创建。Prawitz 的自然推理系统是直觉主义逻辑的一部分,特点是逻辑对称性清楚、明确,从某个角度说是 Gentzen 的串形演算的起点;在机器上执行方便,同时真值在推理过程中的"传递"揭示得非常清楚。所以得到人工智能专家的重视。
  注意到在证明论中,自然推理系统、Gentzen 串形演算、线性逻辑等系统中,主要的对象是证明过程而不是公理系统。特别要注意到的是,在语法上一个推理规则的一点点的增强或者减弱,或者一个规则的删除,都在本质上(语义上、哲学上)导致巨大的差异。这点是需要读者在学习和研究的实践中慢慢体会和理解的。
  在该自然推理系统中,一个证明是一个类似于树形的图,可能有一个或者多个假设,或者没有假设,只含一个结论。
  1.基本概念
  我们将使用形为
        
       A
  的标记来代表一个自然推理的证明。这里A是推理的结论,是一个有穷树的根。该树的"树叶"一种是"有生命的"语句,一种是"无生命的"语句。
  2.推理规则
  (1)前提A
  (2)导入规则
  (3)消除规则

  3.自然推理系统的可计算语义
  将定义一些代数运算,与以上列出的规则一一对应,然后定义代数项。此框架下的代数运算完全与自然推理的证明过程"同构",这就是著名的 " Curry-Howard 同构" 。
  (1) 定义
  (2) 举例,给出逻辑与代数计算的一一同构对应。

  4.Curry - Howard 同构
  已看到自然推理的推理(证明)与函数项之间的一一对应关系,对以下定义一个结构式形式的类型项的集合来说,将成为自然推理的所有推理的集合及这个项的集合之间的一个同构。这就是著名的 Curry - Howard 同构。