zbMATH — the first resource for mathematics

Proof-theoretic aspects of the Lambek-Grishin calculus. (English) Zbl 06484972
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, 109-123 (2015).
Summary: We compare the Lambek-Grishin Calculus (LG) as defined by Moortgat [9, 10] with the non-associative classical Lambek calculus (CNL) introduced by de Groote and Lamarche [4]. We provide a translation of LG into CNL, which allows CNL to be seen as a non-conservative extension of LG. We then introduce a bimodal version of CNL that we call 2-CNL. This allows us to define a faithful translation of LG into 2-CNL. Finally, we show how to accomodate Grishin’s interaction principles by using an appropriate notion of polarity. From this, we derive a new one-sided sequent calculus for LG.
For the entire collection see [Zbl 1319.03010].
03B70 Logic in computer science
Full Text: DOI