Сложность исчисления Ламбека с одним делением и модальностью для ослабления, используемой только при отрицательной полярности

В статье рассматривается вариант исчисления Ламбека, допускающего пустые антецеденты секвенций. В этом варианте используются две связки: левое деление и одноместная модальность, которая встречается только с отрицательной полярностью и разрешает ослабление в антецеденте секвенции. Определяется понятие сети доказательства для этого исчисления, подобное аналогичным сетям для обычного исчисления Ламбека и линейной логики. Доказывается, что произвольная заданная секвенция выводится в рассматриваемом исчислении тогда и только тогда, когда для неё существует сеть доказательства. Найден быстрый (полиномиальный по времени) алгоритм, устанавливающий, выводима ли произвольная данная секвенция в рассматриваемом исчислении.