Research

I am interested in substructural logics, especially in extensions of Nonassociative Lambek Calculus. In particular, I work on extensions being weakenings of linear logic.

Nonassociative Bilinear Logic

Nonassociative Bilinear Logic is Multiplicative-Additive Linear Logic by Girard without the assumptions of associativity and commutativity of the product (multiplicative conjunction). For this logic I provided a left-sided sequent system with cut-elimination property. One may easily obtain right-sided system.

For multiplicative fragment of this logic (i.e. without additive connectives and constants) I proved that pure logic is PTIME.

The decidability of the finitary consequence relation remains an open problem.

Cyclic Nonassociative Bilinear Logic

Cyclic Nonassociative Bilinear Logic is Nonassociative Bilinear Logic, where the linear negations collapse and hence we have only one De Morgan negation (i.e. negation satisfying double negation law). For this logic I provided a left-sided sequent system with cut-elimination property, too.

I showed that this logic is a strongly conservative extension of Full Nonassociative Lambek Calculus (without the additive constants). This theorem remains true for a variant without the multiplicative constants. Moreover, I proved the same result for the associative variants. As a consequence, these theorems hold for the noncyclic versions (described above).

In a paper I showed a constructive proof of that for nonassociative variant. In the paper there is provided an interesting system in which nonlogical axioms are replaced with special rules.

Boolean and Heyting Full Nonassociative Lambek Calculus

Boolean Full Nonassociative Lambek Calculus is an extension of Distributive Full Nonassociative Lambek Calculus with the boolean negation. One may consider this logic as Classical Propositional Calculus extended with Nonassociative Lambek Calculus. For this logic I proved that the finitary consequence relation is EXPTIME.

From the results by Shkatov and Van Alten we know that the finitary consequence relation is EXPTIME-complete, if we do not admit the multiplicative constant.

Heyting Full Nonassociative Lambek Calculus is an extension of Distributive Full Nonassociative Lambek Calculus with the intuitionistic implication or Intuitionistic Propositional Calculus extended with Nonassociative Lambek Calculus. For this logic I proved the same results as above.

The lower bound of complexity for variants with the multiplicative constant remains an open problem.