×

zbMATH — the first resource for mathematics

Proof nets for multiplicative cyclic linear logic and Lambek calculus. (English) Zbl 1456.03092
Summary: 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 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.
MSC:
03F52 Proof-theoretic aspects of linear logic and other substructural logics
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F07 Structure of proofs
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrusci, V. M., Classical conservative extensions of Lambek calculus, Studia Logica, 71, 3, 277-314, (2002) · Zbl 1019.03018
[2] Abrusci, V. M.; Maieli, R., Proceedings of the Conference WoLLIC 2015, 9160, Cyclic multiplicative proof nets of linear logic with an application to language parsing, 53-68, (2015), Bloomington, USA · Zbl 1365.03039
[3] Abrusci, V. M.; Maieli, R., Proceedings of the Conference FG 2015, 9804, Cyclic multiplicative and additive proof nets of linear logic with an application to language parsing, 43-59, (2015), Barcelona: Springer, Barcelona · Zbl 06658630
[4] Abrusci, V. M.; Ruet, P., Noncommutative logic I: the multiplicative fragment, Annals of Pure and Applied Logic, 101, 1, 29-64, (2000) · Zbl 0962.03054
[5] Andreoli, J.-M.; Pareschi, R., Proceedings of Workshop on Substructural Logic and Categorial Grammar, From Lambek Calculus to word-based parsing, (1991), CIS Munchen: Germany, CIS Munchen
[6] Bagnol, M.; Doumane, A.; Saurin, A., Proceedings of the 18th International Conference, FoSSaCS 2015, On the dependencies of logical rules, 436-450, (2015), London, UK · Zbl 1367.03109
[7] Danos, V.; Regnier, L., The structure of multiplicatives, AML, 28, 181-203, (1989) · Zbl 0689.03013
[8] Danos, V., (1990)
[9] de Naurois, P. J.; Mogbil, V., Proceedings of CSL 2007, 4646, Correctness of multiplicative (and exponential) proof structures is NL-complete, 435-450, (2007) · Zbl 1179.03063
[10] Girard, J.-Y., Linear logic, Theoretical Computer Science, 50, 1-102, (1987) · Zbl 0625.03037
[11] Girard, J.-Y.; Ursini, Agliano, Logic and Algebra, Proof nets: the parallel syntax for proof theory, (1995), New York: M. Dekker, New York
[12] Guerrini, S., A linear algorithm for MLL proof net correctness and sequentialization, Theoretical Computer Science, 412, 20, 1958-1978, (2011) · Zbl 1222.03067
[13] Hughes, D.; van Glabbeek, R., Proceedings of the 18th IEEE Logic in Computer Science, Proof nets for unit-free multiplicative-additive linear logic, (2003), Los Alamitos
[14] Lambek, J., The mathematics of sentence structure, The American Mathematical Monthly, 65, 3, 154-170, (1958) · Zbl 0080.00702
[15] Maieli, R., Archive for Mathematical Logic, 42, A new correctness criterion for multiplicative non-commutative proof-nets, 205-220, (2003), Berlin Heidelberg: Springer-Verlag, Berlin Heidelberg · Zbl 1025.03064
[16] Maieli, R., Proceedings of the 14th International Conference LPAR, 4790, Retractile proof nets of the purely multiplicative and additive fragment of linear logic, 363-377, (2007), Berlin Heidelberg: Springer-Verlag, Berlin Heidelberg · Zbl 1137.03324
[17] Maieli, R.; Dowek, G., Proceedings of the International Joint Conference RTA-TLCA, Vienna, 8560, Construction of retractile proof structures, 319-333, (2014), Switzerland: Springer International Publishing, Switzerland · Zbl 1417.03224
[18] Melliès, P.-A.; Ehrhard, T.; Girard, J.-Y.; Ruet, P.; Scott, P., Linear Logic in Computer Science, 316, A topological correctness criterion for multiplicative non-commutative logic, 283-321, (2004), Cambridge University Press
[19] Mogbil, V., Proceedings of CSL 2001, Paris, France, 2142, Quadratic correctness criterion for noncommutative logic, 69-83, (2001), Berlin Heidelberg: Springer-Verlag, Berlin Heidelberg · Zbl 0999.03055
[20] Moot, R.; Retoré, Ch., The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics, 6850, (2012), Berlin Heidelberg: Springer-Verlag, Berlin Heidelberg · Zbl 1261.03001
[21] Moot, R., (2002)
[22] Retoré, C., Traitement Automatique des Langues, 37, 2, Calcul de Lambek et logique linéaire, 39-70, (1996)
[23] Roorda, D., Proof nets for Lambek calculus, Journal of Logic and Computation, 2, 2, 21-233, (1992) · Zbl 0768.03035
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.