Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2.

Voir la notice de l'article provenant de la source Library of Science

In [5] we study Nonassociative Lambek Calculus (NL) augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus (CNL). Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.
Keywords: nonassociative Lambek calculus, linear logic, sequent system, cut elimination, PTIME complexity
@article{BSL_2017_46_1-2_a3,
     author = {Buszkowski, Wojciech},
     title = {Involutive {Nonassociative} {Lambek} {Calculus:} {Sequent} {Systems} and {Complexity}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {46},
     number = {1-2},
     year = {2017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a3/}
}
TY  - JOUR
AU  - Buszkowski, Wojciech
TI  - Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
JO  - Bulletin of the Section of Logic
PY  - 2017
VL  - 46
IS  - 1-2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a3/
LA  - en
ID  - BSL_2017_46_1-2_a3
ER  - 
%0 Journal Article
%A Buszkowski, Wojciech
%T Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
%J Bulletin of the Section of Logic
%D 2017
%V 46
%N 1-2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a3/
%G en
%F BSL_2017_46_1-2_a3
Buszkowski, Wojciech. Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity. Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2. http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a3/