贾　青，贾　阳

(1.中国社会科学院 哲学研究所， 北京　100732； 2.河北师范大学 马克思主义学院，石家庄　050024)



证明网络与语言处理

贾青1，贾阳2

(1.中国社会科学院 哲学研究所， 北京100732； 2.河北师范大学 马克思主义学院，石家庄050024)

证明网络是证明的一种图像处理方式。在范畴语法中，由于证明网络具有便于给出语言句法分析这一特点，因此可以说证明网络是范畴语法中“句法分析即推导”这一口号的最佳体现方式之一。为了对证明网络有一个全面的了解，对其大体内容以及在语言处理上的优势做了概述。

范畴语法；证明网络；语言处理；句法分析

一般来说，在范畴语法(categorial grammar)，特别是范畴类型逻辑(categorial type logic)当中，一个系统会有4种不同的表示方式：自然推演表示、Gentzen表示、树模式表示和公理表示。然而，这4种表示或者推演方式所能表示的证明数量并不一定是相同的，因此就会出现一种表示方式比另一种少的问题。本文中所要介绍的证明网络(proof net)就能解决Gentzen演算中所表示的证明数量少于自然推演这一问题。

由于证明网络是在线性逻辑(linear logic)中发展起来的一种推导的图示表示方式。所以本文第一节中将介绍证明网络与线性逻辑的关系，进而在第二节中介绍兰贝克演算的证明网络表示方式。第三节则将证明网络引入语言分析，最后一节给出一些有待解决的问题和进一步的工作。

一、证明网络与线性逻辑

与自然推演相比，Gentzen演算中所能表示的证明数量要少一些。Gentzen演算与自然推演之间的这种一对多的关系被视为Gentzen演算的一个缺点。……