北京大学期刊网　|　作者　　审稿人　　编委专家　　工作人员 首页　  |  　关于　  |  　浏览　  |  　投稿指南　  |  　新闻公告
 数学进展
 综述文章
 线性逻辑和态极逻辑引论(Ⅰ)(英文) Introduction to Linear Logic and Ludics (Ⅰ) Pierre-Louis Curien Pierre-Louis Curien CNRS & Université Paris Ⅶ (CNRS & Universite Paris VII 收稿日期: 2005-10-25 出版日期: 2005-10-25
 167 浏览 引用导出
0
/   /   推荐
 摘要 《线性逻辑和态极逻辑引论》一文概述了由Girard分别于1986和2001所创建的线性逻辑和态极逻辑.线性逻辑和态极逻辑汲取于计算机科学并反之应用于其中,从根本上对数理逻辑进行了彻底的审视.全文分为两部分.本文是文章的第一部分,致力于线性逻辑的联结词、证明规则、可判定性性质和模型.文章的第二部分将研究证明网并简要介绍态极逻辑.证明网是证明的图式表示,是线性逻辑的主要创新之一. 关键词 ： 切消,  线性逻辑,  计算机科学中的逻辑,  计算的交互模式,  语义,  程序设计语言 Abstract：This two-parts paper offers a survey of linear logic and ludics, which were introduced by Girard in 1986 and 2001, respectively. Both theories revisit mathematical logic from first principles, with inspiration from and applications to computer science. The present part I covers an introduction to the connectives and proof rules of linear logic, to its decidability properties, and to its models. Part II will deal with proof nets, a graph-like representation of proofs which is one of the major innovations of linear logic, and will present an introduction to ludics. Key words： linear logic    logic in computer science    interactive modes of computation    semantics    programming languages
 [1] Pierre-Louis Curien;. 线性逻辑和态极逻辑引论(Ⅱ)(英文)[J]. 数学进展, 2006, 35(1): 1-44. [2] 陈仪香. 谓词转换器的拓扑语义[J]. 数学进展, 2003, 32(2): 221-229. [3] 张国强. 逻辑,语义和计算机科学中的一些基本思想(英文)[J]. 数学进展, 2002, 31(5): 389-402.
Viewed
Full text

Abstract

Cited