Сложность исчислений Ламбека с модальностями и тотальной выводимости в грамматиках

Исчисление Ламбека с единицей можно определить как атомарную теорию (алгебраическую логику) класса моноидов с делениями. Это исчисление, как теория более широкого класса алгебр, чем гейтинговы алгебры, оказывается слабее интуиционистской логики, и в нём отсутствуют структурные правила перестановки, сокращения и ослабления. Рассматриваются расширения исчисления Ламбека модальностями — экспоненциалом, под знаком которого разрешены все структурные правила, и релевантной модальностью, под знаком которой разрешены только правила перестановки и сокращения. Исчисление Ламбека с релевантной модальностью применяется в математической лингвистике. Оба эти расширения алгоритмически неразрешимы. Рассматриваются их фрагменты, в которых модальность может применяться только к формулам хорновой глубины не более $1$. Для этих фрагментов доказывается разрешимость и принадлежность классу NP. Для доказательства, в случае релевантной модальности, вводится новое понятие ${\mathcal{R}}$-тотальной выводимости в контекстно-свободных грамматиках — существование вывода, использующего каждое правило не менее определённого числа раз. Устанавливается NP-полнота задачи ${\mathcal{R}}$-тотальной выводимости для контекстно-свободных грамматик, а также выясняется сложность этой задачи для более общих классов порождающих грамматик.