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...
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.