Description

• Title:
  One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
• Creator:
  Płaczek, Paweł
• Contributor:
  Adam Mickiewicz University, Faculty of Mathematics and Computer Science Uniwersytetu Poznanskiego 4, 61-614 Poznan, Poland;
  pawel.placzek@amu.edu.pl
• Description:
  Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2021.05.05;
  2020.11.13
• Type:
  Other
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;1;
  50
• Subject:
  Substructural logic;
  Lambek calculus;
  nonassociative linear logic;
  sequent system;
  PTime complexity
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/35352 ;
  2449-836X;
  10.18778/0138-0680.2020.25
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  other