摘要
1.从古典逻辑到线性逻辑1986年,法国巴黎第七大学 J。Y.Gi-rard 教授在研究二阶λ-演算的指称语义时发现古典逻辑中的隐含连接词 A(?)B 可以分解成更基本的线性运算!A(?)B,在此基础上,一个与证明论及计算机科学密切相关的新型逻辑系统——线性逻辑(LL)诞生了。由于古典逻辑缺乏切实的方式把证明看成算法,因此是不可构造的,除了不存在任何非平凡的指称语义外,矢列演算中 Cut 的消去也不满足 CR 性质。为了避免这些缺点,
In 1986,J.Y.Girard discovered that usual logical implication could be broken up into more elementary linear operations.Following that,he dev- eloped a new logical system,called linear logic,which appears now as a pr- omising approach to fundamental questions arising in proof theory and in com- puter science.In this paper,we give a brief guide to the characteristics of linear logic,summary the recent developments and discuss the prospect of its applications to computer science.
出处
《计算机科学》
CSCD
北大核心
1991年第1期15-19,41,共6页
Computer Science
