Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2
Cet article a éte moissonné depuis 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},
year = {2017},
volume = {46},
number = {1-2},
language = {en},
url = {http://geodesic.mathdoc.fr/item/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/