这样的表示方法在欧洲广泛使用。特别是近年来人们研究线性逻辑的证明网络中的"legal Path reduction", "regular path reduction" 以求一个 "cut-free" 的证明时，这种记号系统是基本的设置。
在一般情况下，在一个自然推理过程中，一个语句是"活的"，如果它在整个推理中起一个"前提"的作用。比如说，自然推理系统的第一条规则是
A
A本身是"叶"也是根；从逻辑上说我们得到结论A , 因为我们假定了A 。
在一个证明中，某一个作为"叶"的语句有可能变成"无生命的"。因为某一语句的某一出现，在证明中已经不需要了。即是说，假定 T 是一个代表证明的树，以A为根，如果删除某些叶，及某些节点，得到的子树仍然是A的一个证明，那么，可以认为这些"叶"是"无生命的"。一个典型的例子：
(
引入规则)[A]
B
__________
A
B
在这个证明中，B上面虚线中有某一个A的出现，已经构成了A
B
的证明，因而[A]已经不需要了。在计算机执行的形式证明中，对这样的已失效的前提作记录是十分重要的。2．推理规则
（2）导入规则
| a．∧导入 | b.导入 |
c.  导入 |
|
A B |
[A]
B |
A |
| A∧B | AB |
a.A |
| a.∧1 消除 | b.∧2 消除 |
| A∧B ___________ A |
A∧B __________ B |
| c.消除
A A B_____________ B |
d.消除
a.A
_____________ A[t/a] |
3．自然推理系统的可计算语义
（1） 定义
a.由一个假设组成的一个推理（2中的第一条推理规则）以一个变元 x 代表。
b.假定一个推理的最后一步是∧I, 它前面的两个子推理对应于 u[x1,x2,…,xn] 以及
v[x1,x2,…,xn]。那么该推理对应于序对函数 < u[x1,x2,…,xn], v[x1,x2,…,xn] > 。
c.对应于推理规则∧1-消除，假定在这推理步骤之前的子推理是 t[x1,x2,…,xn], 由上，该函数一定是一个序对函数，那么令∧1-消除对应于函数π1(t[x1,x2,…,xn]),π1 是第一变目投影函数，即π1(x1,x2) = x1。同样，与∧2-消除 对应的函数应是π2函数。
d.T 引入规则。如果 v 是此规则上面的子推理对应的项（或函数），如果 A 是已经"失 效了"的前提，那么 v 的形式应是 v[x,x1,x2,…,xn], 这里 x 是对应于 A 的变元。那么，将规则对应为 lx. v[x,x1,x2,…,xn]。
e.T 消除规则。有两个项t[x1,x2,…,xn], u[x1,x2,…,xn] 分别对应于上面的两个子 推理。给定 x1,x2,…,xn 的值，t 是由 A 到 B 的函数， 而 u 是 A 的一个元素，所以 t(u) 是在 B 中的，那么
t[x1,x2,…,xn]u[x1,x2,…,xn]
应该是表达
消除规则的项。由定义 a - e , 有基本等式
a.π1(u,v) = u
b.π2(u,v) = v
c <π1t,π2t> = t
d.(λx.v) = v[x/u]
e.λx.t = t 如果 x 在 t 中不是自由变元。
（2） 举例，给出逻辑与代数计算的一一同构对应。
例1
A B
_____________ 等价于推理 A
A∧B
___________
A
即π1(<x, y >) = x
A
例2[A]
B A
____________ 等价于推理BA A
B__________________
B
左边的函数为 (λx.v(x,y))u(x) = v(u(x),y) .
右边的函数为v(u(x),y)（请自行验证）。
x代表A,y代表B 。
4．Curry - Howard 同构
（1）类型
a. 原子类型 T1,…, Tn是型。
b. 如果 U , V 是型， 则 U→V , U×V 是型。
c. 只有由 a,b 归纳定义出来的对象是型。
（2）项
每一个证明将成为一个项。具体地说，A的一个证明将成为型为A的一个项。
a.变元 x1T , x2T ,…, xnT是型为 T 的项。
b.如果 u,v 分别是型为 U,V 的项，则<u,v> 是型为 U×V 的项。
c.若 t 是型为U×V 的项，则π1(t),π2(t) 是项，型分别为 U , V 。
d.若 v 是型为 V 的项，xU 是一型为 U 的变元，则λxU.v 是型为 U→V 的项。
（那么，约束变元对应于证明中"失效"了的前提）
e. 若 t 及 u 是项，它们的型分别是 U→V 及 U , 则 tu 是一型为 V 的项。
依3（1）只需将变元带上它们相对应的型即可。