Исчисление Ламбека с операцией круллева пересечения — 1

Исчисление Ламбека — это субструктурная логика, т.е. логика без правил сокращения, ослабления и перестановки. Одним из естественных классов моделей для исчисления Ламбека являются модели на алгебрах бинарных отношений ($R$-модели). В рамках доклада будет рассмотрено расширение исчисления Ламбека с помощью операции круллева пересечения, т.е. пересечения степеней данного элемента (начиная с первой). Эта операция в некотором смысле двойственна операции взятия транзитивного замыкания (положительной итерации Клини). В первой части доклада будут доказаны теоремы об устранении сечения, о полноте относительно $R$-моделей, а также верхняя оценка алгоритмической сложности для исчисления Ламбека с операцией круллева пересечения.