This 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 linear logic. 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.
Maieli, R., & Abrusci, V.M. (2019). Proof Nets for Multiplicative Cyclic Linear Logic and Lambek Calculus. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, Volume 29,(Issue 6), 733-762 [10.1017/S0960129518000300].
Titolo: | Proof Nets for Multiplicative Cyclic Linear Logic and Lambek Calculus | |
Autori: | ||
Data di pubblicazione: | 2019 | |
Rivista: | ||
Citazione: | Maieli, R., & Abrusci, V.M. (2019). Proof Nets for Multiplicative Cyclic Linear Logic and Lambek Calculus. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, Volume 29,(Issue 6), 733-762 [10.1017/S0960129518000300]. | |
Handle: | http://hdl.handle.net/11590/340904 | |
Appare nelle tipologie: | 1.1 Articolo in rivista |