Classical non-associative Lambek calculus

被引：18

作者：

De Groote P. ^{[1
]}

Lamarche F. ^{[1
]}

机构：

[1] Projet Calligramme, LORIA UMR no 7503 - INRIA, Campus Scientifique, 54506 Vandœuvre lès Nancy Cedex

来源：

Studia Logica | 2002年 / 71卷 / 3期

关键词：

Linear logic; Non-associative Lambek calculus; Proof-net;

D O I：

10.1023/A:1020520915016

中图分类号：

学科分类号：

摘要：

We introduce non-associative linear logic, which may be seen as the classical version of the non-associative Lambek calculus. We define its sequent calculus, its theory of proof-nets, for which we give a correctness criterion and a sequentialization theorem, and we show proof search in it is polynomial. © 2002 Kluwer Academic Publishers.

引用

页码：355 / 388

页数：33

共 28 条

[1]

Aarts E., Trautwein K., Non-associative Lambek categorial grammar in polynomial time, Mathematical Logic Quaterly, 41, pp. 476-484, (1995)

[2]

Abrusci M., Phase semantics and sequent calculus for pure non-commutative classical linear logic, Journal of Symbolic Logic, 56, 4, pp. 1403-1451, (1991)

[3]

Abrusci M., Maringelli E., A new Correctness Criterion fo Cyclic Multiplicative proof-nets, Journal of Logic, Language and Information, 7, 4, pp. 449-459, (1998)

[4]

Abrusci M., Ruet P., Non commutative logic I: The multiplicative fragment, Annals of Pure and Applied Logic, 101, 1, pp. 29-64, (2000)

[5]

Abrusci V.M., Non-commutative proof-nets, Advances in Linear Logic, London Mathematical Society Lecture Notes, pp. 271-296, (1995)

[6]

Berge C., Graphs, North-Holland, (1985)

[7]

Buszkowski W., Logical Foundations of Ajdukiewicz-Lambek Categorial Grammars, (1989)

[8]

Buszkowski W., Generative power of non-associative Lambek Calculus, Bull. Polish Acad. Sci. Math., 34, pp. 507-516, (1986)

[9]

De Groote Ph., A dynamic programming approach to categorial deduction, Lecture Notes in Artificial Intelligence, 1632, (1999)

[10]

Fleury A., La Règle d'Échange: Logique Lineaire Multiplicative Tressée, (1996)

← 1 2 3 →