Направление исследований 2019-2022 гг.

 - Изучить вопрос об алгоритмической сложности суперинтуиционистских предикатных логик классов конечных шкал фиксированной конечной высоты. Ожидаемым результатом является доказательство того, что для логик классов конечных шкал Крипке (по числу миров) конечной высоты, начиная с высоты три, проблема выполнимости является сигма-0-1-трудной уже в языке с тремя предметными переменными и только одноместными предикатными буквами (предположительно даже для позитивных формул). Аналогичный результат ожидается для логик классов предикатных шкал Крипке с дополнительным требованием постоянства предметных областей. (Рыбаков и Александров)

- Изучить вопрос разрешимости логик конечных предикатных шкал Крипке высоты не более n, где n >= 3, в языке с одноместными предикатными буквами и тремя переменными. Ожидается, что удастся доказать неразрешимость указанных логик. (Александров)

- Продолжить работу по изучению произведений модальных логик в топологической семантики с универсальной модальностью только по одной из координат. Ожидаемый результат: аксиоматизация логики таких произведений в языке с универсальной модальностью. (Мирошниченко)

- продолжить исследование выразимости линейных порядков в арифметике Бюхи. Установить, определимы ли в арифметиках Бюхи неразреженные порядки. Ожидаемый результат: построение интерпретации нестандартной модели арифметики Бюхи в арифметике Бюхи с тем же или согласованным значением параметра. (Запрягаев)

- Продолжить изучение модальных интуиционистских логик. Ожидаемый результат: доказательство полноты логик FS и MIPC полны в топологической семантике. (Кудинов)

- планируется продолжить изучение формализации аксиоматики элементарной геометрии оригами. В частности, планируется построить систему аксиом, основанную на базовом предикате симметрии относительно прямой. (Беклемишев и Лукашов)

- Продолжить изучать вопросы, связанные с алгоритмической сложностью различных расширений исчисления Ламбека, используемых в синтаксическом парсере CatLog3. Одной из целей является поиск более точной оценки сложности для задачи "угадывания скобок" в тех системах, где эта задача разрешима. Для систем, в которых угадывание скобок неразрешимо, планируется найти достаточно богатый фрагмент, на котором задача все-таки будет разрешаться.(Кузнецов)