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