首页 >> 哲学 >> 逻辑学
贾青/贾阳:证明网络与语言处理
2018年05月25日 10:28 来源:《重庆理工大学学报.社会科学》 作者:贾青/贾阳 字号

内容摘要:

关键词:

作者简介:

Proof Net and Language Processing

  作者简介:贾青,中国社会科学院 哲学研究所,北京 100732;贾阳,河北师范大学 马克思主义学院,石家庄 050024 贾青(1984- ),女,河北沧州人,副研究员,博士,研究方向:语言逻辑、哲学逻辑。

  原发信息:《重庆理工大学学报.社会科学》2016年第20169期

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

  Proof net is a kind of image processing for proof.In categorial grammar,proof net,as a kind of syntactic parsingstructure,could be used to analyze nature language.Therefore,it perfectly demonstrates the slogan "parsing as deduction".In order to have a fully understanding of proof net,This paper makes a sketch of its main contents and its advantage in language processing.

  关键词:范畴语法/证明网络/语言处理/句法分析/categorial grammar/proof net/language processing/syntactic parsing

  标题注释:基金项目:国家社会科学基金重大项目“自然语言信息处理的逻辑语义学研究”(10&ZD073)

 

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

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

  一、证明网络与线性逻辑

  与自然推演相比,Gentzen演算中所能表示的证明数量要少一些。Gentzen演算与自然推演之间的这种一对多的关系被视为Gentzen演算的一个缺点。解决这一问题,主要有如下的两个方式:

  [1]引入Gentzen演算的范式(normal form);

  [2]保留Gentzen演算原本的样子,转而使用证明网络这一方式。

  由此,证明网络这一证明的图像处理方式就被引入到问题的解决中来。

  证明网络是在线性逻辑(linear logic)中发展起来的一种推导的图示表示方式,所以在这一节中我们首先介绍一下线性逻辑以及证明网络的关系。

  线性逻辑是一类逻辑系统的统称,其中就包括带乘法的线性逻辑(multiplicative linear logic)。Moot和Retoré指出带乘法的线性逻辑是在兰贝克演算的基础上添加交换性条件后得到的逻辑。为了得到一个单独的回旋(involutive)否定和两个蕴涵(左蕴涵和右蕴涵),我们需要将交换性限制到循环式(cyclic)的交换性上去。如果将带乘法的线性逻辑简称为MLL,那么其证明网络表示中的一些重要定义和结论可被阐述如下:

  在图论中,我们可以将一个图定义为一个二元组〈V,E〉,其中V是图中所有端点的集合,而E则是图中边的集合。

  定义1.1 在一个图G=〈V,E〉中,G的一个匹配(matching)是G本身的一个子图,即由G中的部分端点和部分边构成的集合,这一匹配中每两条边都是不毗连的(没有共同的端点)。

  在一个匹配图中,每一个端点连出的边至多是一条。如果这个端点已连出一条边,那么这个端点就称为已匹配的。

  图G的一个最大匹配是指边数最多的匹配。一个图的最大匹配可能不止一个,但是最大匹配的边数却是确定的且不可能超过图中端点的一半。

  图G的一个完美匹配(perfect matching)是一个包括了图G中原来的所有端点的匹配,是最大匹配的一种。

  定义1.2 一个R&B图是一个边带有颜色的图,其中的边要么是蓝色的(B)要么是红色的(R),而图中的蓝边就定义了一个完美的图匹配。

  对于一个R&B图,我们可以理解为B边对应着公式,而R边则对应着连接词。Moot和Retoré指出上述定义的R&B图表示对证明的图的认识会涉及到可选择的基本路径(alternate elementary path)的问题[1]。

  定义1.3 任意R&B图中的一个路径是一个可选择的基本路径,即这一路径中的边或者是B边或者是R边,但是相同的边不会被使用两次。

作者简介

姓名:贾青/贾阳 工作单位:

转载请注明来源:中国社会科学网 (责编:李秀伟)
W020180116412817190956.jpg
用户昵称:  (您填写的昵称将出现在评论列表中)  匿名
 验证码 
所有评论仅代表网友意见
最新发表的评论0条,总共0 查看全部评论

回到频道首页
QQ图片20180105134100.jpg
jrtt.jpg
wxgzh.jpg
777.jpg
内文页广告3(手机版).jpg
中国社会科学院概况|中国社会科学杂志社简介|关于我们|法律顾问|广告服务|网站声明|联系我们