×

zbMATH — the first resource for mathematics

Cyclic multiplicative proof nets of linear logic with an application to language parsing. (English) Zbl 1365.03039
Paiva, Valeria (ed.) et al., Logic, language, information, and computation. 22nd international workshop, WoLLIC 2015, Bloomington, IN, USA, July 20–23, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-47708-3/pbk; 978-3-662-47709-0/ebook). Lecture Notes in Computer Science 9160, 53-68 (2015).
Summary: This paper concerns a logical approach to natural language parsing based on proof nets (PNs), i.e. de-sequentialized proofs, of linear logic (LL). In particular, it presents a simple and intuitive syntax for PNs of the cyclic multiplicative fragment of linear logic (CyMLL). The proposed correctness criterion for CyMLL PNs can be considered as the non-commutative counterpart of the famous Danos-Regnier (DR) criterion for PNs of the pure multiplicative fragment (MLL) of LL. The main intuition relies on the fact that any DR-switching (i.e. any correction or test graph for a given PN) can be naturally viewed as a seaweed, i.e. a rootless planar tree inducing a cyclic order on the conclusions of the given PN. Dislike the most part of current syntaxes for non-commutative PNs, our syntax allows a sequentialization for the full class of CyMLL PNs, without requiring these latter must be cut-free. Moreover, we give a simple characterization of CyMLL PNs for Lambek Calculus and thus a geometrical (non inductive) way to parse phrases or sentences by means of Lambek PNs.
For the entire collection see [Zbl 1319.03010].

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)
03B65 Logic of natural languages
03B70 Logic in computer science
68T50 Natural language processing
PDF BibTeX XML Cite
Full Text: DOI