Аннотация:Рассматривается исчисление Ламбека с добавленным структурным правилом монотонности (ослабления). Доказывается, что для этого исчисления проблема распознавания выводимости NP-полна (как в присутствии, так и при отсутствии операции умножения). NP-сложность фрагмента без умножения доказывается сведением проблемы SAT к рассматриваемой проблеме.