An application of proof-nets to the study of fragments of the Lambek calculus

AbstractThis paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.

Download Full-text

Proof Nets for the Multimodal Lambek Calculus: From Theory to a Wide-Coverage Categorial Parser

The Logic of Categorial Grammars - Lecture Notes in Computer Science ◽

10.1007/978-3-642-31555-8_7 ◽

2012 ◽

pp. 239-297

Author(s):

Richard Moot ◽

Christian Retoré

Keyword(s):

Lambek Calculus ◽

Proof Nets

Download Full-text

Proof Nets for Lambek Calculus

Journal of Logic and Computation ◽

10.1093/logcom/2.2.211 ◽

1992 ◽

Vol 2 (2) ◽

pp. 211-231 ◽

Cited By ~ 10

Author(s):

DIRK ROORDA

Keyword(s):

Lambek Calculus ◽

Proof Nets

Download Full-text

Generation, Lambek calculus, Montague's semantics and semantic proof nets

10.3115/992730.992737 ◽

2000 ◽

Cited By ~ 2

Author(s):

Sylvain Pogodalla

Keyword(s):

Lambek Calculus ◽

Proof Nets

Download Full-text

Interpolation in fragments of classical linear logic

Journal of Symbolic Logic ◽

10.2307/2275398 ◽

1994 ◽

Vol 59 (2) ◽

pp. 419-444 ◽

Cited By ~ 4

Author(s):

Dirk Roorda

Keyword(s):

Intuitionistic Logic ◽

Linear Logic ◽

Quantum Graphs ◽

Lambek Calculus ◽

Structural Rule ◽

Proof Nets

AbstractWe study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets.

Download Full-text