Моделирование логических систем средствами их фрагментов тема диссертации и автореферата по ВАК РФ 00.00.00, доктор наук Рыбаков Михаил Николаевич

• Рыбаков Михаил Николаевич
• доктор наук
• 2025

Оглавление диссертации доктор наук Рыбаков Михаил Николаевич

Цель работы

Основные результаты

Описание методов

Направления возможного применения методов

Апробация и публикации

I Пропозициональные логики

1 Предварительные сведения

1.1 Необходимые понятия

1.1.1 Пропозициональные языки

1.1.2 Разрешимость и классы сложности

1.1.3 Понятие логики

1.2 Классическая логика высказываний

1.2.1 Синтаксис и семантика

1.2.2 Сложность некоторых задач

2 Модальные логики

2.1 Основные определения и факты

2.1.1 Синтаксис

2.1.2 Семантика Крипке

2.1.3 Логики

2.1.4 Необходимые факты

2.1.5 Удобные обозначения

2.2 Сложность проблемы разрешения

2.2.1 Сложность логик в полном языке

2.2.2 Интервал [K, wGrz]

2.2.3 Анализ доказательства: важные моменты

2.2.4 Интервалы [K, GL] и [K, Grz]

2.2.5 Интервал [K, KTB]

2.2.6 Обсуждение конструкций

2.2.7 Логики линейных шкал

2.3 Ненормальные и квазинормальные логики

2.3.1 Понятия ненормальной и квазинормальной логики

2.3.2 Семантика

2.3.3 Логики

2.3.4 Перенос конструкции

2.3.5 Некоторые замечания

2.4 Сложность аппроксимации

2.4.1 Функция сложности

2.4.2 Полиномиально аппроксимируемые логики

2.4.3 Модальные алгебры

2.5 Замечания

3 Логики Виссера и суперинтуиционистские логики

3.1 Основные определения и факты

3.1.1 Синтаксис

3.1.2 Семантика Крипке

3.1.3 Логики

3.1.4 Необходимые факты

3.1.5 Удобные обозначения

3.2 Сложность проблемы разрешения

3.2.1 Логика BPL

3.2.2 Интервал [BPL, FPL]

3.2.3 Логика Int

3.2.4 Интервал [BPL, KC]

3.2.5 Модальные напарники логики КС

3.3 Сложность аппроксимации

3.3.1 Функция сложности

3.3.2 Полиномиально аппроксимируемые логики

3.3.3 Гейтинговы алгебры

3.4 Замечания

4 Полимодальные логики

4.1 Общие определения

4.1.1 Синтаксис

4.1.2 Семантика Крипке

4.2 Слияния логик и их обогащения

4.2.1 Слияния логик

4.2.2 Логика К*

4.2.3 Логики знания

4.2.4 Логики с универсальной модальностью

4.2.5 Сложность аппроксимации логики К*

4.3 Динамические логики

4.3.1 Предварительные сведения

4.3.2 Синтаксис и семантика

4.3.3 Сложность проблемы выполнимости

4.4 Темпоральные логики

4.4.1 Предварительные сведения

4.4.2 Сложность фрагментов логик СТЬ* и СТЬ

4.4.3 Сложность фрагментов логик АТЬ* и АТЬ

4.4.4 Сложность фрагментов логики ЬТЬ

4.5 Произведения и полупроизведения логик

4.5.1 Предварительные сведения

4.5.2 Синтаксис и семантика

4.5.3 Сложность произведений модальных логик

4.5.4 Сложность полупроизведений модальных логик

4.6 Замечания

II Предикатные логики

5 Классическая логика предикатов

5.1 Синтаксис и семантика

5.2 Неразрешимость

5.2.1 Предварительные сведения

5.2.2 Теорема Чёрча и теорема Трахтенброта

5.2.3 Теории бинарного отношения

5.2.4 Замечания

6 Модальные логики

6.1 Основные определения и факты

6.1.1 Синтаксис

6.1.2 Семантика Крипке

6.1.3 Логики

6.1.4 Необходимые факты

6.1.5 Полимодальный случай

6.2 Неразрешимость логик унарного предиката

6.2.1 Трюк Крипке

6.2.2 Логики с двумя переменными

6.2.3 Замечания

6.3 Разрешимые логики унарных предикатов

6.3.1 Нормальные логики

6.3.2 Ненормальные и квазинормальные логики

6.3.3 Логики с равенством

6.4 Логики элементарно определимых классов шкал

6.4.1 Элементарная определимость классов шкал

6.4.2 Стандартный перевод

6.4.3 Погружения в дСЬ=

6.5 Логики классов шкал, не определимых элементарно

6.5.1 Логики классов конечных шкал

6.5.2 Логики натурального ряда

6.5.3 Логики бесконечных ординалов и плотных порядков

6.5.4 Логики деревьев

6.5.5 Логики шкал логик доказуемости

6.5.6 Контрпримеры

7 Суперинтуиционистские логики

7.1 Основные определения и факты

7.1.1 Синтаксис и семантика Крипке

7.1.2 Логики

7.2 Неразрешимость логик унарного предиката

7.2.1 Трюк Крипке

7.2.2 Позитивные фрагменты с двумя переменными

7.2.3 Позитивные фрагменты с двумя переменными и одним унарным предикатом

7.3 Разрешимые логики унарных предикатов

7.4 Логики первопорядково определимых классов шкал

7.5 Логики конечных моделей

7.5.1 Неперечислимость

7.5.2 Фрагменты с одноместным предикатом

8 Логика квазиарных предикатов

8.1 Основные определения и факты

8.1.1 Предварительные сведения

8.1.2 Синтаксис и семантика

8.2 Алгоритмические свойства

8.2.1 Погружение в классическую логику

8.2.2 Аналоги теоремы Чёрча и теоремы Трахтенброта

8.2.3 Разрешимые фрагменты

Заключение

Библиография

Предметный указатель

Введение

Описание области исследований

Проведённое автором исследование связано с выразительностью языков, логик и теорий, и прежде всего с алгоритмической выразительностью (в том числе вычислительной сложностью) определённых их фрагментов.

Многие естественные логические системы либо алгоритмически неразрешимы (причём иногда сильно неразрешимы), либо, будучи разрешимыми, имеют высокую сложность проблемы разрешения. Известно, что определённые ограничения, накладываемые на средства языка или используемую семантику, приводят к изменению алгоритмической сложности тех или иных задач. В то же время иногда это не так: например, в неклассических логиках как неразрешимость, так и высокая сложность проблемы разрешения в случае разрешимости могут получаться при очень сильных ограничениях на средства языка.

Представляется актуальным не только нахождение границ, в рамках которых подобные проблемы оказываются алгоритмически простыми или наоборот остаются алгоритмически сложными, но и разработка общих методов, позволяющих получать оценки алгоритмической сложности фрагментов не только отдельных логических систем, а всех систем тех или иных бесконечных классов. Вместе с методами хотелось бы иметь общие признаки или критерии, позволяющие сразу говорить об алгоритмической сложности тех или иных фрагментов интересующей нас системы или хотя бы о потенциальной возможности или невозможности применения этих методов.

Подобные исследования проводились как в области пропозициональных систем, так и в области предикатных логик и теорий. В диссертации предложены подходы и методы, позволяющие, в частности, ответить на многие вопросы об

алгоритмической сложности фрагментов различных систем, оставшиеся открытыми в работах исследователей, занимавшихся их изучением.

Проблема разрешения многих «стандартных» модальных пропозициональных логик РБРАСЕ-полна [82,141,257]; то же относится к интуиционистской пропозициональной логике и близким к ней [60,234]. Кроме того, для некоторых модальных логик было установлено, что РБРАСЕ-полным являются даже их фрагменты от одной переменной [77,121,233,238].

Вычислительная сложность проблемы разрешения таких логик оказалась тесно связана с вопросами сложности их аппроксимации шкалами Крипке. Вопросы о сложности аппроксимации неклассических логик были поставлены А. В. Кузнецовым [11,140] в контексте интуиционистской логики. При этом сам А. В. Кузнецов предполагал, что интуиционистская логика полиномиально аппроксимируема, а следовательно, полиномиально разрешима, и даже предложил конструкцию, позволяющую полиномиально погрузить интуиционистскую логику в классическую в предположении справедливости этой гипотезы [11]. Чуть позже М. В. Захарьящевым и С. В. Поповым было показано, что интуиционистская логика не является полиномиально аппроксимируемой [6]; то же справедливо и для модальных логик.

Тем не менее, фрагмент интуиционистской логики от одной переменной является полиномиально разрешимым, что следует из конструкции Ригера-Ниши-муры [164, 173]. Сложность фрагментов от большего числа переменных была неизвестна [82, проблема 18.4], и А. В. Чагровым высказывалась гипотеза о том, что каждый из этих фрагментов является полиномиально аппроксимируемым, а значит, полиномиально разрешимым.

Автор диссертации начал исследование этих вопросов под руководством А. В. Чагрова примерно в 2001 году. В ходе исследований были получены результаты, касающиеся сложности проблемы разрешения для бесконечных семейств неклассических логик; кроме того, как для логик в полном языке, так и для их фрагментов в языке с конечным числом переменных, были получены результаты, касающиеся сложности их аппроксимации шкалами Крипке, а также связи сложности аппроксимации с вычислительной сложностью проблемы разрешения. Возникшие в ходе исследований методы были затем перенесены на полимодальные пропозициональные логики [48, 66,178,190, 199, 206, 208, 209] и

предикатные логики [10,45,50,65,135,182,193,201,202,204,205,207].

Классическая логика предикатов дС1 алгоритмически неразрешима [85,242] (более точно, Х^-полна [124]). Область исследования вопросов разрешимости её фрагментов известна как «классическая проблема разрешения» [79]: имеется огромное количество результатов, дающих как разрешимые, так и неразрешимые фрагменты логики дС1, классических теорий первого порядка, а также других формальных предикатных систем [107,117,119,128,129,132,137,138,156, 157, 237, 255]. Так, чтобы доказать неразрешимость логики дС1, достаточно, чтобы её язык содержал одну бинарную предикатную букву и три предметные переменные [241]. В то же время, следующие фрагменты логики дС1 разрешимы:

• монадический фрагмент, даже обогащённый равенством [78];

• различные охраняемые фрагменты [117,157];

• фрагмент с двумя предметными переменными [119,156].

Неразрешимы также и многие первопорядковые теории, в частности, теории в языке лишь с одной бинарной предикатной буквой: например, теория симметричного иррефлексивного бинарного отношения (это извлекается из конструкций, приведённых в [137,159]) и, как следствие, теория симметричного рефлексивного бинарного отношения. Что касается теорий конечных моделей, они могут даже не быть рекурсивно перечислимыми [58,59] (похожие результаты для других языков можно найти, например, в [75,120]).

Алгоритмическая неразрешимость модальных предикатных логик мгновенно следует из неразрешимости классической логики предикатов. Для доказательства неразрешимости классической логики предикатов требуются предикатные буквы валентности не менее чем два, а также как минимум три предметные переменные. Поэтому возникает вопрос об алгоритмической сложности монадических фрагментов модальных предикатных логик, а также их фрагментов от не более чем двух предметных переменных. Фрагменты от одной предметной переменной могут быть разрешимы: как было замечено Д. М. Габбаем и В. Б. Шехтманом [107], из [218] следует разрешимость фрагмента логики д85 от одной предметной переменной, а аналогичный результат для д84 следует

из [103]; кроме того, в [68] доказана разрешимость фрагмента от одной предметной переменной логики QGL. Поэтому особый интерес представляет вопрос о разрешимости фрагментов с двумя предметными переменными, в частности, монадических.

Известно, что, в отличие от монадического фрагмента классической логики предикатов, монадические фрагменты модальных предикатных логик во многих «естественных» случаях алгоритмически неразрешимы, причём для соответствующего доказательства достаточно, чтобы их язык содержал две унарные предикатные буквы и бесконечно много предметных переменных [138] или две предметные переменные и бесконечно много унарных предикатных букв [107,132].

Из неразрешимости классической логики предикатов QCl следует и неразрешимость интуиционистской предикатной логики QInt, поскольку QCl погружается в QInt. Известно, что монадический фрагмент QInt неразрешим, и даже при одной унарной букве в языке [15,105], а также известно, что неразрешим фрагмент QInt с двумя предметными переменными [107, 132]. Разрешимость фрагмента QInt с одной предметной переменной следует из разрешимости аналогичного фрагмента модальной логики QS4.

В диссертации показано, что эти результаты о неразрешимости можно усилить и распространить на большой класс логик, включающий как модальные и суперинтуиционистские предикатные логики, так и расширения предикатных вариантов базисной и формальной логик Виссера. При этом предложены общие методы, позволяющие моделировать бинарные предикатные буквы унарными (в духе метода Крипке [138] для модальных логик), а также унарные предикатные буквы формулами от одной унарной предикатной буквы.

Кроме того, в диссертации довольно большое внимание уделено вопросам алгоритмической сложности логик элементарно неопределимых классов шкал Крипке. Известно, что если логика (любая, в том числе модальная, суперинтуиционистская, пропозициональная, предикатная) полна относительно элементарно определимого класса шкал Крипке, то такая логика погружается в классическую логику предикатов [25,109,246], а следовательно, является рекурсивно перечислимой. Если же логика полна по Крипке, но при этом не полна относительно элементарно определимого класса шкал Крипке, то такая логика до-

вольно часто не является рекурсивно перечислимой.

Имеются элементарно неопределимые классы шкал Крипке, содержащие в том числе бесконечные шкалы, модальные предикатные логики которых представляют определённый интерес. Например, к такого рода «естественным» классам относятся классы конечных шкал Крипке той или иной логики, различные классы деревьев, а также классы шкал таких логик как дОЬ, дОг7, QwGrz и других.

В диссертации рассмотрены логики, определяемые такого рода классами шкал Крипке, и продемонстрированы методы, позволяющие доказывать, что эти логики сильно неразрешимы даже при очень бедных средствах языка. Это позволило извлечь некоторые следствия, в том числе касающиеся полноты по Крипке различных исчислений и их фрагментов.

Введение диссертации (часть автореферата) на тему «Моделирование логических систем средствами их фрагментов»

Цель работы

Основная цель работы состоит в том, чтобы развить общие методы моделирования алгоритмически сложных проблем внутри логик и теорий минимальными средствами языка. В частности, в работе предложены методы моделирования полных языков их ограниченными средствами, позволяющие получить погружения логик и теорий в соответствующие их фрагменты; в большинстве случаев эти погружения оказываются полиномиально вычислимыми.

Сопутствующая цель работы состоит в том, чтобы показать, что при дальнейшем ограничении средств языков подобные моделирования становятся невозможными. Таким образом, вместе с разработкой методов получается и описание своего рода границ возможности их применения.

К средствам языка, которые минимизируются, в первую очередь относятся следующие: число пропозициональных переменных в пропозициональных языках, число предметных переменных, а также число и валентность предикатных букв в языках первого порядка. Рассматриваются и некоторые ограничения на использование логических связок и кванторов.

Отметим, что попутно удаётся решить и другие задачи, не попадающие в рамки описанных целей работы. Так, в качестве одного из следствий получены результаты о неполноте по Крипке бесконечных классов модальных исчислений

первого порядка, причём даже при сильных ограничениях на средства языка.

Основные результаты

В диссертации представлены результаты об алгоритмической сложности фрагментов как пропозициональных [178,179, 199,200,208,212], так и предикатных [50,181,182,201-205,210,211] логик. Ниже используются стандартные обозначения для логик и формул [82,109]; знак «+» понимается как объединение множеств формул с последующим замыканием по правилам modus ponens, обобщения и подстановки, а знак «0» — как объединение множеств формул с последующим замыканием по правилам modus ponens, обобщения, подстановки и усиления.

Теорема 1 (результат представлен в [179]). Пусть Int С L С KC. Тогда позитивный фрагмент от двух переменных логики L является PSPACE-трудным.

Теорема 2 (результат представлен в [208]). Произведения и полупроизведения логик, первый сомножитель которых равен K, T, KB или KTB, полиномиально погружаются в свой фрагмент от одной переменной.

Это даёт возможность получить ряд результатов об алгоритмической сложности фрагментов от конечного числа переменных для больших классов логик, учитывая результаты о сложности произведений логик в полном языке [127,149].

Теорема 3 (результат представлен в [208]). Пусть логика L такова, что K х K х K С L С KTB х S5 х S5. Тогда фрагмент логики L в языке с одной пропозициональной переменной неразрешим.

Теорема 4 (результат представлен в [208]). Пусть K х K С L С KTB х S5. Тогда фрагмент логики L в языке с одной пропозициональной переменной является coNEXPTIME-трудным.

Последнее утверждение имеет следующее уточнение, касающееся нескольких конкретных логик.

Теорема 5 (результат представлен в [208]). Фрагменты от одной переменной логик K х K, K х K4 и K х S52 неэлементарны.

Для динамических логик получены следующие результаты.

Теорема 6 (результат представлен в [199]). Константный фрагмент логики PDL является EXPTIME-полным, причём в языке с одной элементарной программой и итерацией.

Теорема 7 (результат представлен в [199]). Константный фрагмент логики IPDL является 2ЕХРТ1МЕ-полным, причём в языке с одной элементарной программой.

Теорема 8 (результат представлен в [199]). Константный фрагмент логики PRSPDL является неразрешимым.

Использованная техника моделирования переменных формулами от их фиксированного конечного числа позволяет получить экспоненциальную нижнюю оценку функции сложности для соответствующих фрагментов PSPACE-трудных мономодальных логик.

Тем не менее, прямой связи между сложностью аппроксимации логики и вычислительной сложностью проблемы её разрешения нет.

Теорема 9 (результат представлен в [212]). Для любой степени неразрешимости существует нормальное линейно аппроксимируемое расширение логики K4, проблема принадлежности формул и проблема принадлежности константных формул которому имеют эту степень неразрешимости.

Теорема 10 (результат представлен в [212]). Пусть L £ {KTB, GL, Grz}. Для любой степени неразрешимости существует нормальное линейно аппроксимируемое расширение логики L, проблема принадлежности формул и проблема принадлежности формул от одной переменной которому имеют эту степень неразрешимости.

Теорема 11 (результат представлен в [212]). Для любой степени неразрешимости существует линейно аппроксимируемое расширение логики Int, проблема принадлежности формул и проблема принадлежности формул от двух переменных которому имеют эту степень неразрешимости.

Теперь опишем основные результаты, полученные для модальных и суперинтуиционистских предикатных логик.

Теорема 12 (результат представлен в [50]). Пусть Ь — модальная предикатная логика, содержащая QCl и содержащаяся в QS5, QGL 0 0 bf, QGrz 0 bd2 0 bf, QGL.3 0 bf или QGrz.3 0 bf. Тогда фрагмент логики Ь в языке с одной унарной предикатной буквой алгоритмически неразрешим.

Этот результат позже был усилен для очень многих логик. Именно, была получена следующая теорема.

Теорема 13 (результат представлен в [201]). Пусть Ь — модальная предикатная логика, содержащая QCl и содержащаяся в QKTB, QGL 0 bf или QGrz 0 bf. Тогда фрагмент логики Ь в языке с одной унарной предикатной буквой и двумя предметными переменными алгоритмически неразрешим.

В доказательстве было существенным, что у логики имеются сколь угодно большие (и даже бесконечные) шкалы. Следующие наблюдения показывают, что это условие действительно является важным.

Теорема 14 (результат представлен в [50]). Пусть Ь — модальная предикатная логика, определяемая одной конечной шкалой Крипке. Тогда монадиче-ский фрагмент логики Ь алгоритмически разрешим.

Теорема 15 (результат представлен в [213]). Для любого п Е N монадиче-ские фрагменты логик QAltn, QTAltn, QAltn 0 bf и QTAltn 0 bf алгоритмически разрешимы.

Аналогичные результаты получены для монадических фрагментов модальных предикатных логик с равенством.

В целом, в случае логик бесконечных классов конечных шкал Крипке ситуация с разрешимостью иная.

Теорема 16 (результат представлен в [202]). Пусть Ь — модальная предикатная логика, содержащая QCl и содержащаяся в QS5, QGL.3 или QGrz.3. Тогда фрагменты

логик ЬтАп и ЬтАп 0 bf в языке с тремя предметными переменными является одновременно Е®-трудным и П\-трудным.

Отметим, что при этом дополнительно можно потребовать, чтобы язык логики Ь не содержал предикатных букв, кроме некоторой бинарной буквы.

Для монадических фрагментов модальных предикатных логик классов конечных шкал был получен следующий результат.

Теорема 17 (результат представлен в [202]). Пусть Ь — модальная предикатная логика, содержащая QC1 и содержащаяся в QKTB, QGL или QGrz. Тогда фрагменты логик Ьщап и ЬтАп ф bf в языке с одной унарной предикатной буквой и тремя предметными переменными является П\-трудным.

Близкие результаты были получены и для суперинтуиционистских предикатных логик, а также предикатных вариантов базисной и формальной логик Виссера [251], которые обозначим QBL и QFL соответственно.

Теорема 18 (результат представлен в [201]). Пусть QBL С Ь С QKC или QBL С Ь С QFL. Тогда позитивный фрагмент логики Ь алгоритмически неразрешим в языке с одной унарной предикатной буквой и двумя предметными переменными.

Для суперинтуиционистских логик классов конечных шкал Крипке получаются результаты, сходные с модальным случаем.

Теорема 19 (результат представлен в [205]). Пусть Ь — суперинтуиционистская предикатная логика, содержащая в QLC. Тогда позитивные фрагменты логик Ьуфп и Ьуфп + ей в языке с тремя предметными переменными являются одновременно -трудными и П\-трудными.

Теорема 20 (результат представлен в [205]). Пусть Ь — суперинтуиционистская предикатная логика, содержащая в QKC. Тогда позитивные фрагменты логик Ьуфп и Ьуфп + ей в языке с одной унарной предикатной буквой и тремя предметными переменными является П\-трудным.

Используемые методы могут быть распространены и на логики, задаваемые другими классами шкал, не определимыми элементарно. В диссертации представлены результаты исследования алгоритмических свойств модальных предикатных логик некоторых линейных порядков, а также нётеровых порядков.

Теорема 21 (результат представлен в [204]). Пусть а = ш • т+к — ординал, где 1 ^ т < ш и к < ш. Пусть Я — бинарное отношение на а, лежащее между отношениями < и ^, где отношение < — естественный строгий порядок на а, а отношение ^ — его рефлексивное замыкание. Тогда модальная предикатная логика шкалы Крипке {а, Я) является П\-трудной в языке с одной унарной предикатной буквой, одной пропозициональной буквой и двумя предметными переменными.

Отметим, что использованное моделирование позволяет попутно получить результаты, касающиеся алгоритмической сложности монадических фрагментов логик шкал Крипке <), (К, <), (К, и некоторых других. Именно, логики таких шкал Е0-трудны в языке с одной унарной буквой, одной пропозициональной буквой и двумя предметными переменными. Известно [89], что логикой шкалы Крипке является аксиоматическая система QS4.3, а логикой шкалы Крипке <) — система QK4.3.D.X, и мы можем заключить, что указанные фрагменты этих логик Е0-полны.

Теперь скажем о результатах, полученных для логик нётеровых порядков. Для модальной предикатной логики Ь определим модальную предикатную логику Ь* как логику класса шкал Крипке логики Ь.

Теорема 22 (результат представлен в [182]). Пусть модальная предикатная логика Ь такова, что QwGrz* С Ь, а также Ь С QGL.3* 0 bf или Ь С QGrz.3* 0 bf. Тогда фрагмент логики Ь в языке с одной унарной предикатной буквой, одной пропозициональной буквой и тремя предметными переменными является П \ -трудным.

Теорема 23 (результат представлен в [182]). Пусть модальная предикатная логика Ь такова, что QwGrz* С Ь, а также Ь С QGL.3* 0 bf или Ь С QGrz.3* 0 bf. Тогда фрагмент логики Ь в языке с двумя унарными предикатными буквами, одной пропозициональной буквой и двумя предметными переменными является П -трудным.

Теорема 24 (результат представлен в [182]). Пусть модальная предикатная логика Ь такова, что QwGrz* С Ь, а также Ь С QGL* 0 bf или

Ь С QGrz* ф bf. Тогда фрагмент логики Ь в языке с одной унарной предикатной буквой, одной пропозициональной буквой и двумя предметными переменными является П\-трудным.

Как следствие получаем неполноту по Крипке всех рекурсивно перечислимых логик между QwGrz и QGL.3фbf, а также между QwGrz и QGrz.3фbf (неполнота по Крипке некоторых из этих логик получена ранее в [155], но другими методами), причём даже их соответствующих фрагментов.

С учётом этих результатов возникает вопрос о существовании рекурсивно перечислимых полных по Крипке модальных предикатных логик, не задаваемых элементарно определеимыми классами шкал Крипке. Примеры таких логик были построены.

Теорема 25 (результат представлен в [203]). Существуют полные по Крип-ке рекурсивно перечислимые модальные предикатные логики, которые неполны относительно элементарно определимых классов шкал.

Описание методов

Были использованы как общие методы, так и специальные. К общим методам относятся различные общематематические методы (например, часто использовавшийся метод математической индукции), а также синтаксический и семантический методы (например, активно использовалась семантика Крипке), методы теории алгоритмов, методы теории вычислительной сложности, методы теории решёток, методы теории замощений. Мы не будем давать подробных пояснений к этим методам, и остановимся подробнее на специальных методах.

• Был использован метод, предложенный Дж. Халперном [121], позволяющий моделировать пропозициональные переменные языка формулами от одной пропозициональной переменной. Этот метод был сначала обобщён в классе пропозициональных логик [178, 199, 200, 208] (в частности, в некоторых случаях подобное моделирование удалось получить с помощью константных формул), а затем модифицирован и применён в классе модальных предикатных логик [65,182,201,202,207].

• Был использован метод моделирования переменных языка формулами от одной переменной, предложенный П. Блэкбёрном и Э. Спаан [77]. Модификации этого метода хорошо показали себя в исследованиях, связанных с модальными предикатными логиками, определяемыми линейными шкалами Крипке [204].

• Был предложен метод моделирования пропозициональных переменных интуиционистского языка формулами от двух переменных [179]. Затем этот метод был перенесён на суперинтуиционистские предикатные логики [202,205].

• Был использован и модифицирован метод С. Крипке [138], позволяющий моделировать бинарные предикатные буквы в классических предикатных формулах с помощью модальности и унарных предикатных букв [50]. Этот метод был перенесён на различные классы модальных и суперинтуиционистских предикатных логик, а также на предикатные варианты базисной и формальной логик Виссера [202,205].

• Были использованы методы моделирования укладки домино [74,124], описанные в работах Ф. Волтера, М. Захарьящева, Р. Кончакова и А. Ку-руш [132,255], с помощью модификаций которых были получены результаты о неразрешимости и сильной неразрешимости модальных и суперинтуиционистских предикатных логик [182,204].

• Был использован стандартный перевод модальных предикатных формул в формулы языка классической логики предикатов [25,109,246], позволивший получить один из результатов работы [203].

• Был модифицирован метод доказательства разрешимости монадического фрагмента классической логики предикатов [78], что позволило получить верхнюю границу алгоритмической сложности неклассических предикатных логик, определяемых классами конечных шкал Крипке [50].

Направления возможного применения методов

Результаты и методы исследований могут быть перенесены на другие классы логик. Приведём несколько примеров.

Начнём с пропозициональных логик. Касающиеся их результаты содержатся в работах [178,179,199,200,208,212], и вполне разумно говорить о дальнейшем применении соответствующих методов.

• Было бы интересно распространить описанные методы на релевантные [175,244,245] и интуиционистские модальные логики [103,165]. Частично это сделано, и уже получены некоторые результаты.

• Было бы интересно выявить такие ситуации и такие логики, когда методы моделирования переменных языка формулами от фиксированного конечного числа переменных не работают, а также понять, какова в каждом из случаев сложность проблемы разрешения.

При этом некоторые исследования уже проведены. Упомянем некоторые из полученных результатов.

• Удалось распространить результат о Р8РЛСЕ-трудности константных фрагментов модальных логик [84] на класс всех логик, лежащих между К и wGrz [63].

• Сколь угодно сложные линейно аппроксимируемые логики найдены в классах ненормальных и квазинормальных логик [51], а также в классах расширений базисной и формальной логик Виссера.

• Построены полиномиальные погружения модальных интуиционистских логик в их фрагменты от одной переменной [197,215].

• Построены погружения логики HC (известной как логика совместных задач и высказываний [151,152]) в её фрагменты от одной переменной; доказано, что эти фрагменты Р8РЛСЕ-полны [18].

Теперь скажем о предикатных логиках. Здесь видится довольно много вопросов, оставшихся за рамками вошедших в диссертацию научных работ.

• В классе неклассических предикатных логик остались нерешёнными вопросы об алгоритмической сложности «стандартных» логик в языке с одной предметной переменной, логик классов конечных шкал Крипке в языке с двумя предметными переменными, а также многих других логик,

определяемых «естественными» элементарно неопределимыми классами шкал Крипке. Результаты работы показывают, что здесь можно ожидать разное: такие логики могут быть как рекурсивно перечислимыми в полном языке, так и сильно неразрешимыми в довольно бедном фрагменте языка.

• Доказано (но публикаций на момент написания этого текста ещё нет), что множество общезначимых формул первого порядка в языке с бинарной предикатной буквой и тремя предметными переменными рекурсивно неотделимо от множества формул в том же языке, опровергающихся в классе конечных моделей, где бинарная предикатная буква интерпретируется симметричным иррефлексивным бинарным отношением. Это даёт возможность существенно расширить класс модальных и суперинтуиционистских предикатных логик, для которых известно, что их фрагмент от одной унарной предикатной буквы и трёх предметных переменных неразрешим.

• В. Б. Шехтманом был поставлен вопрос о рекурсивной отделимости мона-дических фрагментов модальных предикатных логик и дополнений логик, определяемых классами конечных шкал Крипке исходных логик. Развитые в диссертации методы позволяют исследовать этот вопрос, и первые результаты в этом направлении уже имеются [38,183].

• Идеи доказательства разрешимости монадических фрагментов логик, определяемых одной конечной шкалой Крипке, были перенесены на логики с равенством. В результате удалось доказать разрешимость их мона-дических фрагментов с равенством при различных пониманиях равенства; аналогичные результаты были получены для полимодальных и суперинтуиционистских логик [65,213].

• Кроме того, были получены обобщения конструкции Крипке [138], позволяющей моделировать бинарные предикатные буквы языка с помощью модальности и унарных предикатных букв [214].

• Была доказана неразрешимость фрагмента предикатного варианта логики Гёделя-Дамметта QLC в языке с двумя предметными переменными (этот вопрос долго был открыт; см., например, [80]), причём не только для логи-

ки QLC, но и для бесконечного класса её расширений; для доказательства использовался язык с бинарной предикатной буквой и бесконечным множеством унарных [39,184] или же две бинарные предикатные буквы [40].

Апробация и публикации

На основе результатов исследований были сделаны доклады на научных семинарах, а также российских и международных конференциях [2,3,7-9,18-40,65, 83,84,176,177,186-198]. Научные центры, где были сделаны выступления в рамках научных семинаров: ТвГУ, ИФ РАН, МГУ имени М. В. Ломоносова, МИАН, ИМ СО РАН, НИУ ВШЭ, МФТИ, IRIT (Тулуза, Франция), WITS (Йоханнесбург, ЮАР). Кроме того, некоторые из ранних результатов вошли в кандидатскую диссертацию автора [41] и некоторые более поздние — в PhD thesis [185].

По теме диссертации опубликованы научные работы [4,10,42-57,63,66,134, 135,178-182,199-212,215]. Исследования продолжаются, и имеются работы, направленные в печать.

Часть I

Пропозициональные логики

Глава 1

Предварительные сведения

1.1 Необходимые понятия 1.1.1 Пропозициональные языки

Как правило, для определения пропозициональных формул используются языки, содержащие бесконечное множество исходных символов (обычно требуется наличие бесконечного множества пропозициональных переменных). В то же время алгоритмы работают со словами, записанными с помощью символов конечных алфавитов. Таким образом, чтобы формулы формально могли быть поданы на вход алгоритмам, нужно, чтобы они строились в языке с конечным числом исходных символов.

Для этих целей зафиксируем алфавит РА:

РА = [р,1,ш, |, (,)}.

Пусть N = {0,1, 2,... } — множество натуральных чисел, — множество положительных натуральных чисел. Для всякого п Е N обозначим

п+ 1

т. е. 0 = |, 1 = ||, 2 = ||| и т. д.

Слово вида p(n) будем называть пропозициональной переменной и вместо записи «p(n)» будем использовать более привычную — «pn». Аналогично тому,

как использовалась буква р для определения пропозициональных переменных, будем использовать букву / для определения логических связок. Именно, в качестве логических связок будем использовать слова вида /(к)(п), записывая их более коротко как /П, где к — валентность (арность) связки /П, а п — её номер. Букву т будем использовать для определения модальностей, считая их выражениями вида т(к)(п) и записывая более коротко как тП, где к — валентность (арность) модальности ткп, а п — её номер.

В результате логические связки Л, V, ^ могут быть определены, например, так: ± = /0, Л = /0, V = /2, ^ = Одноместная модальность □ п может быть определена как тП. При необходимости в качестве индексов модальностей можно использовать не только коды натуральных чисел, но и иные выражения. Так, например, в динамических логиках используются одноместные модальности вида [а], где а — некоторое выражение, называемое программой. В этом случае модальность [а] можно определить формально как выражение т(1)(а), при необходимости расширяя исходный алфавит, чтобы ввести определение программы.

Далее мы не будем уделять большого внимания подобным техническим подробностям, полагая, что приведённых здесь пояснений достаточно для того, чтобы было понятно, как дать соответствующие формальные определения; важным является лишь то, что все рассматриваемые здесь формулы и языки могут быть определены с использованием подходящего конечного алфавита.

1.1.2 Разрешимость и классы сложности

Формально под алгоритмами мы будем понимать машины Тьюринга или иную эквивалентную формализацию понятия алгоритма, см. например, [1, 5, 13,16]. Фактически мы будем пользоваться интуитивным понятием алгоритма, принимая при этом тезис Чёрча-Тьюринга, состоящий в том, что всякая функция, вычислимая алгоритмически в интуитивном смысле, вычислима с помощью некоторой машины Тьюринга.

Далее речь пойдёт только о задачах принадлежности множествам слов. Содержательно, под задачей принадлежности слов в алфавите 2 множеству А будем понимать задачу, состоящую в следующем: по произвольному слову х

выяснить, принадлежит ли х множеству А. Формально задачу принадлежности слов множеству А будем отождествлять с самим множеством А, и далее будем использовать как понятие «множество слов», так и «задача».

Множество слов А в некотором алфавите Е называем разрешимым, или рекурсивным, если существует такая алгоритмически вычислимая функция1 /: Е* ^ {0,1}, что для каждого слова х в алфавите Е

,, , I 1, если х Е А, I(х) = <

; 1 0, если х Е А,

т. е. если существует алгоритм, выясняющий по каждому слову в Е, принадлежит ли оно множеству А; в противном случае множество А называем неразрешимым .

Множество слов А в некотором алфавите Е называем рекурсивно перечислимым , если А = 0 или существует такая алгоритмически вычислимая функция /: N ^ Е*, что

А = {/(п) : п Е

т. е. если существует алгоритм, перечисляющий элементы множества А.

Множество А слов в алфавите А называется разрешимым относительно множества В слов в алфавите В, если существует алгоритм с оракулом во множестве В, решающий задачу принадлежности множеству А; говорят также, что А рекурсивно относительно В. Наличие оракула во множестве В означает, что алгоритм в процессе своей работы может «вычислять» характеристическую функцию множества В. Если А разрешимо относительно В, то пишем А ^ В.

Множество А слов в алфавите А называем рекурсивно эквивалентным множеству В слов в алфавите В, если А ^ В и В ^ А; в этом случае пишем А В. Класс [А]к = {В : В А} называем2 степенью неразрешимости.

Содержательно, степень неразрешимости состоит из таких множеств, что если у нас появится способ выяснения принадлежности элементов одному из них,

хПод функцией понимаем всюду определённую функцию.

2При введении дополнительных ограничений — например, требуя, что слова всех рассматриваемых множеств определяются над одним и тем же конечным алфавитом — можно добиться того, чтобы возникающий класс оказался множеством. В литературе в подобных ситуациях часто рассматривают подмножества множества N. Для нас это будет несущественно, т.к. мы будем рассматривать весьма ограниченный класс задач (связанных с множествами формул в тех или иных языках), и он является множеством; кроме того, нам будет интересен не столько этот класс сам по себе, сколько отдельные задачи.

то это даст возможность получить такой способ и для любого другого множества из этой степени неразрешимости. Степени неразрешимости называются также степенями Тьюринга, или T-степенями, а возникающее отношение — тью-ринговой сводимостью, или T-сводимостью.

Несмотря на то, что T-сводимость довольно полно отражает интуитивное понятие сводимости разрешимости одной задачи к другой, имеются другие, более сильные, сводимости.

Задача A в алфавите A называется рекурсивно сводимой к задаче B в алфавите B, если существует такая вычислимая функция f: A* ^ B*, что для всякого x Е A*

x Е A ^^ f (x) Е B.

Рекурсивная сводимость известна также как т-сводимость3. Если задача A m-сводима к задаче B, то пишем A B. Для множества A можно определить4 т-степень [A]m = {B : A B и B A}.

Заметим, что если A B, то A ^r B; обратное, вообще говоря, неверно: если A — алфавит, то 0 A*, но 0 A*.

Пусть C — некоторый класс неразрешимых задач. Задача A называется C-трудной, если к ней m-сводима любая задача из класса C. Задача A называется C-полной, если она принадлежит классу C и при этом является C-трудной.

Примерами классов неразрешимых задач являются арифметическая иерархия и аналитическая иерархия, см. [174]. Обычно и ту, и другую определяют не через алгоритмы, а через арифметические формулы, задействуя язык арифметики первого порядка в случае арифметической иерархии и язык арифметики второго порядка в случае аналитической иерархии. В арифметической иерархии нас будут интересовать в основном класс П0 и класс S0, а точнее, П0-трудные и £0-трудные задачи. Сами задачи при этом мы будем рассматривать не для множеств натуральных чисел, а для множеств формул; чтобы было возможно так делать, формально вместо формул можно, например, брать их гёделевы номера [16], отождествляя формулы с ними. В приводимых ниже построениях и доказательствах мы не будем уделять внимания обсуждению подобных технических деталей, т.е. не будем обращаться к гёделевой нумерации явно. В анали-

Список литературы диссертационного исследования доктор наук Рыбаков Михаил Николаевич, 2025 год

Библиография

[1] Булос Дж., Джеффри Р. Вычислимость и логика. Москва, Мир, 1994.

[2] Горбунов И. А., Рыбаков М. Н. Выразительность операторов знания и возможность эффективного описания логик знания // Проблемы управления и моделирования в сложных системах. Труды III Международной конференции, Самара, Самарский научный центр РАН, 2001, с. 617-622.

[3] Гусева А. С., Рыбаков М. Н. Интуиционистские формулы от двух переменных и PSPACE-полнота // Современная логика: проблемы теории, истории и применения в науке. Материалы VIII Общероссийской научной конференции, Санкт-Петербург, 2004, с. 480-482.

[4] Духовнева А. В., Рыбаков М.Н., Шкатов Д. П. Алгоритмическая выразительность некоторых фрагментов языка логики ветвящегося времени // Программные продукты и системы, 29(4):135-142, 2016.

[5] Ершов Ю.Л., Палютин Е.А. Математическая логика. Издание второе. Москва, Наука, 1987.

[6] Захарьящев М.В., Попов С. В. О мощности контрмоделей интуиционистского исчисления // Препринт ИПИ АН СССР, 45, 1980.

[7] Котикова Е. А., Рыбаков М. Н. Сложность проблемы истинности константных модальных формул в модели // Современная логика: проблемы теории, истории и применения в науке. Материалы XI Общероссийской научной конференции, Санкт-Петербург, 2010, с. 281-283.

[8] Котикова Е. А., Рыбаков М. Н. Предикатная логика ветвящегося времени QCTL: алгоритмические, семантические и дедуктивные аспекты //

10

11 12

13

14

15

16

17

18

Открытый Российско-Финский коллоквиум по логике, Санкт-Петербург, 2012.

Котикова Е.А., Рыбаков М.Н. Алгоритмическая выразительность предикатной логики ветвящегося времени в языке с одной одноместной буквой // Десятые Смирновские чтения по логике, Москва, 2017, с. 43-44.

Котикова Е. А., Рыбаков М. Н. Моделирование арифметики в языке первого порядка, обогащенном темпоральными кванторами // Вестник ТвГУ. Серия: Прикладная математика, 4:5-19, 2016.

Кузнецов А. В. О средствах для обнаружения невыводимости или невыразимости // Логический вывод. М., Наука, 1979, с. 5-33.

Левин Л. А. Универсальные задачи перебора // Проблемы передачи информации, т. 9, №3, 1973, с. 115-116.

Мальцев А. И. Алгоритмы и рекурсивные функции. Москва, Наука, 1965.

Мардаев С. И. Вложения импликативных решеток в суперинтуиционистские логики // Алгебра и логика, т. 26, №3, 1987, с. 318-357.

Маслов С.Ю., Минц Г. Е., Оревков В. П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Доклады АН СССР, 163(2):295-297, 1965.

Мендельсон Э. Введение в математическую логику. Москва, Наука, 1976.

Оноприенко А. А. Семантика типа Крипке для пропозициональной логики задач и высказываний // Математический сборник, 211(5):98-125, 2020.

Оноприенко А. А., Рыбаков М. Н. Сложность логики НС с одной переменной // Международная конференция Мальцевские чтения. Тезисы докладов. Новосибирск, 2024, с. 44.

Рыбаков М.Н., Чагров А. В. Модальные формулы без переменных и РБРАСЕ-полнота // Современная логика: проблемы теории, истории и

применения в науке. Материалы VII Международной научной конференции, Санкт-Петербург, 2002, с. 498-500.

[20] Рыбаков М.Н., Чагров А. В. О сложности модальных логик, имеющих доказуемостную интерпретацию, с ограничениями на число переменных // Колмогоров и современная математика, Москва, 2003, с. 707-708.

[21] Рыбаков М.Н., Шкатов Д. П. Существование рекурсивно перечислимой полной по Крипке нормальной модальной предикатной логики, которая не полна относительно первопорядково определимых классов шкал // Одиннадцатые Смирновские чтения по логике, Москва, 2019, с. 43-45.

[22] Рыбаков М. Н., Шкатов Д. П. Трюк Крипке и разрешимость монадических фрагментов модальных и суперинтуиционистских предикатных логик // Тринадцатые Смирновские чтения по логике. Материалы международной научной конференции. Москва, 2023, с. 40-44.

[23] Рыбаков М. Н. Консервативность в нормальных модальных предикатных логиках // Тезисы XXXVII Международной научной студенческой конференции, Новосибирск, Издательство НГУ, 1999.

[24] Рыбаков М. Н. Разрешимость интуиционистской логики предикатов относительно классической логики предикатов // Современная логика: проблемы теории, истории и применения в науке. Материалы VI Международной научной конференции. Санкт-Петербург, 2000, с. 247-250.

[25] Рыбаков М.Н., Чагров А. В. Стандартные переводы неклассических формул и относительная разрешимость логик // Труды научно-исследовательского семинара Логического центра Института философии РАН, 14, Москва, 2000, с. 81-98.

[26] Рыбаков М. Н. О степени неразрешимости предикатных логик знания // Труды научно-исследовательского семинара Логического центра Института философии РАН, 15, Москва, 2001, с. 79-91.

[27] Рыбаков М. Н. Рекурсивная сводимость предикатных вариантов стандартных модальных логик к классической логике предикатов // Российской

математике — триста лет. Материалы юбилейной научной конференции. Тверь, 2002, с. 108-114.

[28] Рыбаков М. Н. О сложности проблемы разрешения для базисной и формальной логик с конечным числом переменных в языке // Смирновские чтения. IV Международная конференция. Москва, 2003, с. 49-50.

[29] Рыбаков М.Н. Формальная предикатная логика А.Виссера: выразительность фрагментов языка от одной одноместной буквы // Современная логика: проблемы теории, истории и применения в науке. Материалы IX Общероссийской научной конференции. Санкт-Петербург, 2006, с. 386-388.

[30] Рыбаков М.Н. К вопросу о полноте по Крипке предикатных логик // Смирновские чтения. Материалы 5-й конференции. Москва, 2007, с. 3738.

[31] Рыбаков М. Н. Неклассические логики: их сложность и сложность их приложений // Философия математики: актуальные проблемы. Материалы Международной научной конференции, Москва, 2007, с. 123-125.

[32] Рыбаков М. Н. Свойства логик знания при одновременном использовании оператора распределённого знания и оператора всеобщего знания // Современная логика: проблемы теории, истории и применения в науке. Материалы X Общероссийской научной конференции. Санкт-Петербург, 2008, с. 443-444.

[33] Рыбаков М. Н. Сложность фрагментов логики 1РЭЬ // Шестые Смирновские чтения по логике, 2009, с. 34-35.

[34] Рыбаков М. Н. Погружение классической логики предикатов в логику квазиарных предикатов // Девятые Смирновские чтения по логике, Москва, 2015, с. 33-34.

[35] Рыбаков М. Н. Неразрешимость модальных предикатных логик в языке с одной одноместной буквой // Десятые Смирновские чтения по логике, Москва, 2017, с. 41-43.

[36] Рыбаков М.Н., Шкатов Д. П. Неразрешимость логик с унарным предикатом и двумя переменными // Математические основы информатики и информационно-коммуникационных технологий. Сборник трудов, Тверь, 2021, с. 246-254.

[37] Рыбаков М.Н. Undecidability of modal and superintuitionistic logics of a single unary predicate in languages with two variables // Вторая конференция Математических центров России. Аннотации докладов, Москва, 2022, с. 73-74.

[38] Рыбаков М.Н. Рекурсивная неотделимость в модальных и суперинтуиционистских предикатных логиках // Мальцевские чтения. Тезисы докладов, СО РАН, Новосибирск, 2023, с. 16.

[39] Рыбаков М.Н. Неразрешимость логики QLC в языке с двумя предметными переменными //IV Конференция математических центров России. Сборник тезисов, 2024, с. 151-152.

[40] Рыбаков М.Н., Серова Д. А. Неразрешимые фрагменты расширений предикатной логики Гёделя-Дамметта // Международная конференция Мальцевские чтения. Тезисы докладов, СО РАН, Новосибирск, 2024, с. 45.

[41] Рыбаков М. Н. Сложность пропозициональных логик с конечным числом переменных. Диссертация на соискание учёной степени кандидата физико-математических наук. Тверь, 2005.

[42] Рыбаков М. Н., Чагров А. В. Константные формулы в модальных логиках: проблема разрешения // Логические исследования, 9:202-220, 2002.

[43] Рыбаков М. Н. Разрешимость некоторых модальных предикатных логик относительно классической логики предикатов // Учёные записки Тверского государственного университета, 6, Тверь, 2000, с. 8-12.

[44] Рыбаков М. Н. Перечислимость модальных предикатных логик и условия обрыва возрастающих цепей // Логические исследования, 8:155-167, 2001.

[45] Рыбаков М. Н. Об алгоритмической выразительности модального языка с одной лишь одноместной предикатной буквой // Логические исследования, 9:179-201, 2002.

[46] Рыбаков М. Н. Сложность проблемы разрешения базисной и формальной логик // Логические исследования, 10:158-166, 2003.

[47] Рыбаков М. Н. Погружение интуиционистской логики в её фрагмент от двух переменных и сложность этого фрагмента // Логические исследования, 11:247-261, 2004.

[48] Рыбаков М. Н. Сложность константного фрагмента пропозициональной динамической логики // Вестник ТвГУ. Серия: Прикладная математика, 5:5-17, 2007.

[49] Рыбаков М. Н. Неразрешимость логики квазиарных предикатов // Вестник ТвГУ. Серия: Прикладная математика, 4:17-32, 2014.

[50] Рыбаков М. Н. Неразрешимость модальных логик одноместного предиката // Логические исследования, 23(2):60-75, 2017.

[51] Рыбаков М.Н. Алгоритмические свойства линейно аппроксимируемых квазинормальных модальных логик // Вестник ТвГУ. Серия: Прикладная математика, 4:87-97, 2018.

[52] Рыбаков М. Н. Аксиоматизируемость ненормальных и квазинормальных модальных предикатных логик первопорядково определимых классов шкал Крипке // Вестник ТвГУ. Серия: Прикладная математика, 3:81-94, 2018.

[53] Рыбаков М. Н. Сложность проблемы равенства слов в многообразиях модальных алгебр // Вестник ТвГУ. Серия: Прикладная математика, 3:5-17, 2021.

[54] Рыбаков М. Н. Алгоритмическая сложность теорий бинарного предиката в языках с малым числом переменных // Доклады Российской академии наук. Математика, информатика, процессы управления, 507(6):61-65, 2022.

[55] Рыбаков М. Н. Сложность проблемы равенства слов в модальных и псевдобулевых алгебрах с малым числом порождающих // Известия вузов. Математика, 5:42-60, 2022.

[56] Рыбаков М.Н. Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино? // Логические исследования, 29(1):114-146, 2023.

[57] Рыбаков М. Н. Деревья как средство моделирования неразрешимых проблем // Вестник ТвГУ. Серия: Прикладная математика, (1):5-23, 2023.

[58] Трахтенброт Б. А. Невозможность алгорифма для проблемы разрешимости на конечных классах // Доклады АН СССР, 70(4):569-572, 1950.

[59] Трахтенброт Б. А. О рекурсивной отделимости // Доклады АН СССР, 88:953-956, 1953.

[60] Чагров А. В. О сложности пропозициональных логик // Сложностные проблемы математической логики. Калинин, КГУ, 1985, с. 80-90.

[61] Шехтман В. Б. Двумерные модальные логики // Математические заметки, 23(5):759-772, 1978.

[62] Янков В. А. Об исчислении слабого закона исключенного третьего // Известия АН СССР. Сер. матем., 2(5):1044-1051, 1968.

[63] Agadzhanian I., Rybakov M. Complexity of the variable-free fragment of the weak Grzegorczyk logic. arXiv:2211.14571, 2022.

[64] Alechina N., Demri S., de Rijke M. A modal perspective on path constraints. Journal of Logic and Computaion, 13(6):939-956, 2003.

[65] Agadzhanian I., Rybakov M., Shkatov D. Algorithmic complexity of monadic multimodal predicate logics with equality over finite Kripke frames. In: SCAN 2023 Semantical and Computational Aspects of Non-Classical Logics. Moscow + Online, June 13-17, 2023, pages 16-19, Moscow, 2023. Steklov International Mathematical Center.

[66] Aleksandrov K., Rybakov M., Shkatov D. Computational complexity of one-variable fragments of products with T. arXiv:2112.03833, 2021.

[67] Alur R., Henzinger T. A., Kuperman O. Alternating-time temporal logic. Journal of ACM, 49(5):672-713, 2002.

[68] Artemov S., Dzhaparidze G. Finite Kripke models and predicate logics of provability. The Journal of Symbolic Logic, 55(3):1090-1098, 1990.

[69] Artemov S., Protopopescu T. Intuitionistic epistemic logic. Review of Symbolic Logic, 9(2):266-298, 2016.

[70] Baader F., Calvanese D., McGuinness D.L., Nardi D., Patel-Schneider P. F. The Description Logic Handbook: Theory, Implementation, Applications. Cambridge University Press, Cambridge, UK, 2003.

[71] Balbiani P., Tinchev T. Definability and computability for PRSPDL. In: Advances in Modal Logic, 10:16-33, 2014.

[72] Behmann H. Beitraige zür Algebra der Logik, inbesondere zum Entscheidungsproblem. Mathematische Annalen, 86:163-229, 1922.

[73] Bennett B., Cohn A. G., Wolter F., Zakharyaschev M. Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Applied Intelligence, 17:239-251, 2002.

[74] Berger R. The Undecidability of the Domino Problem, volume 66 of Memoirs of AMS. AMS, 1966.

[75] Bianchi M., Montagna F. Trakhtenbrot theorem and first-order axiomatic extensions of MTL. Studia Logica, 103:1163-1181, 2015.

[76] Blackburn P., deRijke M., Venema Y. Modal Logic. Cambridge University Press, 2001.

[77] Blackburn P., Spaan E. A modal perspective on the computational complexity of attribute value grammar. Journal of Logic, Language, and Information, 2:129-169, 1993.

[78] Boolos G.S., Burgesss J. P., Jeffrey R. C. Computability and Logic. Cambridge University Press, fifth edition, 2007.

[79] Borger E., Gradel E., Gurevich Y. The Classical Decision Problem. Springer, 1997.

[80] Caicedo X., Metcalfe G., Rodriguez R., Tuyt O. One-variable fragments of intermediate logics over linear frames. Information and Computation, 287, 2022.

[81] E. Carpinska. On Intermediate Logics Which Can Be Axiomatized by Means of Implicationless Formulas. Reps Math. Logic, No. 13, 1981, p.11-16.

[82] Chagrov A., Zakharyaschev M. Modal Logic. Oxford University Press, 1997.

[83] Chagrov A.V., Rybakov M.N. Least number of variables for PSPACE-hardness of provability problem in systems of modal logic. In: Advances in Modal Logic. 30 Septembre - 2 Octobre 2002. Institut de Reacherche en Informatique de Toulouse, Universite Paul Sabatier, Toulouse, France, pages 178-188, Toulouse, 2002.

[84] Chagrov A.V., Rybakov M.N. How many variables one needs to prove PSPACE-hardness of modal logics? In: Advances in Modal Logic, 4:71-82, London, 2003. King's College Publications.

[85] Church A. A note on the "Entscheidungsproblem". The Journal of Symbolic Logic, 1:40-41, 1936.

[86] Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using Branching Time Temporal Logic. In: Proceedings of Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981.

[87] Clarke E. M., Grumberg O., Peled D. A. Model Checking. MIT Press, 2000.

[88] Cook S. A. The Complexity of Theorem-Proving Procedures. Proceedings of the Third Annual ACM Symposium on the Theory of Computation, 1971, p. 151-158.

[89] Corsi G. Quantified modal logics of positive rational numbers and some related systems. Notre Dame Journal of Formal Logic, 34(2):263-283, 1993.

[90] Cresswell M. J. The completeness of S1 and some related systems. Notre Dame Journal of Formal Logic, 13(4):485-496, 1972.

[91] David A. Deciding ATL* by tableaux. In: Amy P. Felty and Aart Mid-deldorp, editors, Automated Deduction-CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 214-228, 2015.

[92] De Giacomo G., Lenzerini M. Boosting the correspondence between description logics and propositional dynamic logics. In: Proceeding of the Twelfth National Conference on Artificial Intelligence (AAI'94), 1:205-212, AAI Press, 1994.

[93] Del Cerro F. L., Orlowska E. DAL—a logic for data analysis. Theoretical Computer Science, 36:251-264, 1985.

[94] Demri S., Goranko V., Lange M. Temporal Logics in Computer Science: Finite-state systems, volume 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.

[95] Demri S., Schnoebelen P. The complexity of propositional linear temporal logics in simple cases. Information and Computation, 174:84-103, 2002.

[96] Diego A. Sur les algebres de Hilbert. Gauthier-Villars, Paris, 1966.

[97] Donini F.M., Lenzerini M., Nardi D., Nutt W. The complexity of concept languages. Information and Computation, 134(1):1-58, 1997.

[98] Emerson E. A. Halpern J. Y. Decision procedures and expressiveness in temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1-24, 1985.

[99] Emerson E. A. Halpern J.Y. "Sometimes and Not Never" revisited: on Branching versus Linear Time Temporal Logic. Journal of ACM, 33(1):151-178, 1986.

[100] Fagin R., Halpern J. Y., Moses Y., Vardi M. Y. Reasoning About Knowledge. MIT Press, 1995.

101 102

103

104

105

106

107

108

109

110

Fine K. An ascending chain of S4 logics. Theoria, 40(2):110-116, 1974.

Fischer M. J., Ladner R. E. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194-211, 1979.

Fischer Servi G. On modal logic with an intuitionistic base. Studia Logica, 36(3):141-149, 1977.

Gabbay D.M.. The Decidability of the Kreisel-Putnam System. The Journal of Symbolic Logic, 35(3):431-437, 1970.

Gabbay D. Semantical Investigations in Heyting's Intuitionistic Logic. D. Reidel, 1981.

Gabbay D., Kurucz A., Wolter F., Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2003.

Gabbay D., Shehtman V. Undecidability of modal and intermediate firstorder logics with two individual variables. The Journal of Symbolic Logic, 58(3):800-823, 1993.

Gabbay D., Shehtman V. Products of modal logics, Part 1. Logic Journal of the IGPL, 6(1):73-146, 1998.

Gabbay D., Shehtman V., Skvortsov D. Quantification in Nonclassical Logic, Volume 1. Volume 153 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2009.

Gabelaia D., Kurucz A., Wolter F., Zakharyaschev M. Products of 'transitive' modal logics. The Journal of Symbolic Logic, 70(3):993-1021, 2005.

Gabelaia D., Kurucz A., Wolter F., Zakharyaschev M. Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic, 142(1-3):245-268, 2006.

[112] Goldblatt R. Logics of Time and Computation, volume 7 of CSLI Lecture Notes. Center for the Study of Language and Information, second edition, 1992.

[113] Goller S., Jung J.-C., Lohrey M. The complexity of decomposing modal and first-order theories. ACM Transactions on Computational Logic, 9(4):Arti-cle 39, 2010.

[114] Goranko V., Shkatov D. Tableau-based decision procedure for full coali-tional multiagent temporal-epistemic logic of linear time. In: C. Sierra, C. Castelfranchi, K. S. Decker, and J. Sichman, editors, Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 09), pages 969-976, 2009.

[115] Goranko V., Shkatov D. Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Transactions on Computational Logic, 11(1):3-51, 2009.

[116] Goranko V., van Drimmelen G. Complete axiomatization and decidability of the alternating-time temporal logic. Theoretical Computer Science, 353(1-3):93-117, 2006.

[117] Gradel E. On the restraining power of guards. Journal of Symbolic Logic, 64(4):1719-1742, 1999.

[118] Gradel E., Otto M., Rosen E. Undecidability results on two-variable logics. Archive for Mathematical Logic, 38:313.

[119] Gradel E., Kolaitis P. G., Vardi M.Y. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997.

[120] Hajek P. Trakhtenbrot theorem and fuzzy logic. In: G. Gottlob, E. Grandjean, and K. Seyr, editors, International Workshop on Computer Science Logic. CSL98, volume 1584 of Lecture Notes in Computer Science, pages 1-8, 1998.

[121] Halpern J. Y. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence, 75(2):361-372, 1995.

[122] Halpern J. Y., Moses Y. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54(3):319-379, 1992.

[123] Halpern J.Y., Vardi M.Y. The complexity of reasoning about knowledge and time I: Lower bounds. Journal of Computer and System Sciences, 38(1):195-237, 1989.

[124] Harel D. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. Journal of the ACM, 33:224-248, 1986.

[125] Harel D., Sherman R. Looping versus repeating in dynamic logic. Information and Control, 55:175-192, 1982.

[126] Hirsch R., Hodkinson I. Representability is not decidable for finite relation algebras. Transactions of the American Mathematical Society, 353:14031425, 2001.

[127] Hirsch R., Hodkinson I., Kurucz A. On modal logics between K x K x K and S5 x S5 x S5. The Journal of Symbolic Logic, 67(1):221-234, 2002.

[128] Hodkinson I., Wolter F., Zakharyaschev M. Decidable fragments of firstorder temporal logics. Annals of Pure and Applied Logic, 106:85-134, 2000.

[129] Hodkinson I., Wolter F., Zakharyaschev M. Monodic fragments of first-order temporal logics: 2000-2001 A.D. In: R. Nieuwenhuis and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Volume 2250 of Lecture Notes in Computer Science, pages 1-23. Springer, 2001.

[130] Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2nd edition, 2004.

[131] Kontchakov R., Kurucz A., Wolter F., Zakharyaschev M. Spatial logic + temporal logic = ? In M. Aiello, I. Pratt-Hartmann, and J. Van Benthem, editors, Handbook of Spatial Logics, pages 497-564. Springer, 2007.

[132] Kontchakov R., Kurucz A., Zakharyaschev M. Undecidability of first-order intuitionistic and modal logics with two variables. Bulletin of Symbolic Logic, 11(3):428-438, 2005.

[133] Kornilowicz A., Ivanov I., Nikitchenko M. Kleene algebra of partial predicates. Formalized Mathematics, 26(1):11-20, 2018.

[134] Kotikova E. A., Rybakov M.N. First-order logics of branching time: On expressive power of temporal operators. Логические исследования, 19:6899, 2013.

[135] Kotikova E. A., Rybakov M.N. Kripke incompleteness of first-order calculi with temporal modalities of CTL and near logics. Логические исследования, 21(1):86-99, 2015.

[136] Kracht M. Syntactic codes and grammar refinement. Journal of Logic, Language, and Information, 4:41-60, 1995.

[137] Kremer P. On the complexity of propositional quantification in intuitionistic logic. The Journal of Symbolic Logic, 62(2):529-544, 1997.

[138] Kripke S.A. The undecidability of monadic modal quantification theory. Zeitschrift für Matematische Logik und Grundlagen der Mathematik, 8:113116, 1962.

[139] Kurucz A. Combining modal logics. In: P. Blackburn, J. Van Benthem, and F. Wolter, editors, Handbook of Modal Logic. Volume 3 of Studies in Logic and Practical Reasoning, pages 869-924. Elsevier, 2008.

[140] Kuznetsov A. V. On superintuitionistic logics. In: Proceedings of the International Congress of Mathematicians, pages 243-249. Vancouver, 1975.

142

143

144

145

146

147

148

149

150

151

Ladner R. E. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467-480, 1977.

Lange M., Lutz C. 2-EXPTIME lower bound for propositional dynamic logic with intersection. The Journal of Symbolic Logic, 70(4):1072-1086, 2005.

Lewis H. R., Papadimitriou c. H. Elements of the Theory of Computation. Prentice-Hall, 2nd edition, 1998.

Libkin L. lements of Finite Model Theory. Springer, 2004.

Litak T. The non-reflexive counterpart of Grz. Bulletin of the Section of Logic, 36(3-4):195-208, 2007.

Lowenheim L. Uber Moglichkeiten im Relativkalktil. Mathematische An-nalen, 76(4):447-470, 1915.

Lutz C. Complexity and succinctness of public announcement logic. In: H. Nakashima, M. P. Wellman, G. Weiss, and P. Stone, editors, Proceedings of 5th International Joint Conference on Autonomous Agents and Multiagent Systems, pages 137-143, 2006.

Lutz C., Wolter F., Zakharyaschev M. Temporal description logics: A survey. In: 15th International Symposium on Temporal Representation and Reasoning, pages 3-14, 2008.

Marx M. Complexity of products of modal logics. Journal of Logic and Computation, 9(2):197-214, 1999.

Marx M., Mikulas S. Products, or how to create modal logics of high complexity. Logic Journal of the IGPL, 9(1):71-82, 2001.

Melikhov S. A. A Galois connection between classical and intuitionistic logics. I: Syntax, 2013-2017, arXiv:1312.2575.

Melikhov S. A. A Galois connection between classical and intuitionistic logics. II: Semantics, 2015-2018, arXiv:1504.03379.

[153] Massacci F. Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity. In: B. Nebel, editor, Proceedings of the seventeenth International Conference on Artificial Iintelligence, pages 193-198. Morgan Kaufmann, 2001.

154] Mendelson E. Introduction to Mathematical Logic. CRC Press, sixth edition, 2015.

155] Montagna F. The predicate modal logic of provability. Notre Dame Journal of Formal Logic, 25(2):179-189, 1984.

156] Mortimer M. On languages with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, pages 135-140, 1975.

157] Motohashi N. A decision method for a set of first order classical formulas and its applications to decision problem for non-classical propositional logics // J. Math. Soc., vol. 42, No. 1, Japan, 1990.

158] Nagle M. C., Thomason S. K. The extensions of the modal logic K5. Journal of Symbolic Logic, 50(1):102-109, 1975.

159] Nerode A., Shore R. A. Second order logic and first order theories of re-ducibility ordering. In: J. Barwise, H. J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 181-200. North-Nolland, 1980.

160] Nikitchenko M.S., Tymofieiev V. G. Satisfiability and validity problems in many-sorted composition-nominative pure predicate logics. In: V. Er-molayev, H. Mayr, M. Nikitchenko, A. Spivakovsky, and G. Zholtkevych, editors, ICT in Education, Research, and Industrial Applications. ICTERI 2012, volume 347 of Communications in Computer and Information Science. Springer, 2012.

[161] Nikitchenko M., Shkilniak S. Semantic properties of logics of quasiary predicates. In: Proceedings of the Workshop on Foundations of Informatics F0I-2015, pages 180-197, 2015.

162]

163]

164]

165]

166]

167]

168]

169]

170]

171]

172]

173]

174]

Nikitchenko M., Shkilniak S. Algebras and logics of partial quasiary predicates. Algebra and Discrete Mathematics, 23(2):263-278, 2017.

Nikitchenko M., Shkilniak S. Pure first-order logics of quasiary predicates. Problems in Programming, pages 73-86, 2018.

Nishimura I. On formulas of one variable in intuitionistic propositional calculus. The Journal of Symbolic Logic, 25(4):327-331, 1960.

Prior A. Time and Modality. Clarendon Press, Oxford, 1957.

Papadimitriou C. H. Computational Complexity. Addison-Wesley, 1994.

Peleg D. Concurrent dynamic logic. Journal of the ACM, 34(2):450-479, 1987.

Plaza J. A. Logics of public communications. In: M. L. Emrich, M. S. Pfeifer, M. Hadzikadic, and Z. W. Ras, editors, Proceedings of the fourth international symposium on methodologies for intelligent systems: Poster session program, pages 201-216, 1989.

Pnueli A. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-67, 1977.

Post E. L. Recursively enumerable sets of positive integers and their decision problems. Bull. Amer. Math. Soc., 50(5):284-316, 1944.

Reynolds M. A tableau for CTL*. In: Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Lecture Notes in Computer Science, pages 403-418. Springer, 2009.

Reynolds M., Zakharyaschev M. On the products of linear modal logics. Journal of Logic and Computation, 11(6):909-931, 2001.

Rieger L. On the lattice theory of Brouwerian propositional logic. Acta Facultatis Rerum Naturalium Universitatis Carolinae, 189:1-40, 1952.

Rogers H. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.

[175] Routley R., Meyer R. K. The semantics of entailment. In: Hugues Leblanc, editor, Truth, Syntax and Modality, volume 68 of Studies in Logic and the Foundations of Mathematics, pages 199-243. Elsevier, 1973.

[176] Rybakov M.N. Complexity of the two-variable fragment of intuitionistic propositional logic. In: Computer Science Applications of Modal Logic. International Conference. Moscow, September 5-9 2005, pages 35-36, Moscow, 2005. Poncelet Laboratory of UMI 2615 and Independent University of Moscow.

[177] Rybakov M.N. Complexity of intuitionistic and visser's basic and formal logics in finitely many variables. In: Advances in Modal Logic, 6:393-411, London, 2006. College Publications.

[178] Rybakov M.N. Complexity of finite-variable fragments of EXPTIME-complete logics. Journal of Applied Non-Classical Logics, 17(3):359-382, 2007.

[179] Rybakov M. N. Complexity of intuitionistic propositional logic and its fragments. Journal of Applied Non-Classical Logics, 18(2-3):267-292, 2008.

[180] Rybakov M. Computational complexity of the word problem in modal and Heyting algebras with a small number of generators. Russian Mathematics, 66(5):33-48, 2022.

[181] Rybakov M. Computational complexity of theories of a binary predicate with a small number of variables. Doklady Mathematics, 106(3):458-461, 2022.

[182] Rybakov M. Predicate counterparts of modal logics of provability: High undecidability and Kripke incompleteness. Logic Journal of the IGPL, 32(3):465-492.

[183] Rybakov M. Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate. arXiv:2505.00524, 2025.

[184] Rybakov M. Superintuitionistic predicate logics of linear frames: undecid-ability with two individual variables. arXiv:2505.00531, 2025.

[185] Rybakov M. Algorithmic properties of modal logics with restricted languages. PhD thesis, University of the Witwatersrand, Johannesburg, 2019.

[186] Rybakov M., Serova D. Tiling problems and complexity of logics. In: SCAN 2023 Semantical and Computational Aspects of Non-Classical Logics. Moscow + Online, June 13-17, 2023, pages 70-72, Moscow, 2023. Steklov International Mathematical Center.

[187] Rybakov M., Shkatov D. Computational complexity of logics of nontermi-nating programs with restrictions on the number of propositional variables.

In: В. И. Маркин, editor, Девятые Смирновские чтения по логике. Москва, Современные тетради, 2015, с. 34.

[188] Rybakov M., Shkatov D. On existence of recursively-enumerable Kripke-complete first-order modal logics that are not Kripke complete with respect to a first-order definable class of frames. In: Десятые Смирновские чтения по логике, Москва, Современные тетради, 2017, с. 45.

[189] Rybakov M., Shkatov D. Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables. In: T. Uustalu B. Fischer, editor, Lecture Notes in Computer Science, volume 11187, pages 396-414. Springer-Verlag GmbH, 2018.

[190] Rybakov M., Shkatov D. On complexity of propositional linear-time temporal logic with finitely many variables. In: B. Haskins J. van Niekerk, editor, Proceedings of SAICSIT18. South Africa, Port Elizabeth, 26-28 September 2018, pages 313-316. ACM, 2018.

[191] Rybakov M., Shkatov D. A recursively enumerable Kripke complete firstorder logic not complete with respect to a first-order definable class of frames. In: George Metcalfe, Guram Bezhanishvili, Giovanna D'Agostino and Thomas Studer, editors, Advances in Modal Logic, 12:531-540. College Publications, 2018.

[192] Rybakov M., Shkatov D. Trakhtenbrot theorem for classical languages with three individual variables. In: Proceedings of the South African Institute of Computer Scientists and Information Technologists 2019. Skukuza, South Africa, September 17-18, 2019, New York, NY, USA, ACM, Article No. 19.

2019.

[193] Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of the natural number line in restricted languages. In: Sara Negri Nicola Olivetti, Rineke Verbrugge and Gabriel Sandu, editors, Advances in Modal Logic. 978-1-84890-341-8. Helsinki, August 24-28. July 2020, 13:523-539. College Publications, 2020.

[194] Rybakov M., Shkatov D. Computational properties of the logic of partial quasiary predicates. In: Conference of the South African Institute of Computer Scientists and Information Technologists 2020. September 14-16,

2020. Cape Town, South Africa, pages 58-65, ACM, New York, NY, USA, 8 pages, 2020.

[195] Rybakov M., Shkatov D. Algorithmic properties of QK4.3 and QS4.3. In:

Ю. В. Ивлев В. И. Шалак Н. Е. Томова; отв.ред. В. И. Маркин О. М. Григорьев, Д. В. Зайцев, editor, Двенадцатые Смирновские чтения, с. 50-54, Москва, 2021. Русское общество истории и философии науки.

[196] Rybakov M., Shkatov D. On relationship between complexity function and complexity of validity in propositional modal logic. In: Logical Perspectives

2021. Moscow, June 7 - July 8, 2021.

[197] Rybakov M., Shkatov D. On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics. In: SCAN 2023 Semantical and Computational Aspects of Non-Classical Logics. Moscow + Online, June 13-17, 2023, pages 73-76. Steklov International Mathematical Center, 2023.

[198] Rybakov M., Shkatov D., Skvortsov D. On the system of positive slices in the structure of superintuitionistic predicate logics. In: Agata Ciabattoni, David Gabelaia, and Igor Sedlar, editors, Advances in Modal Logic, 15:653674. College Publications, 2024.

[199] Rybakov M., Shkatov D. Complexity and expressivity of propositional dynamic logics with finitely many variables. Logic Journal of the IGPL, 26(5):539-547, 2018.

[200] Rybakov M., Shkatov D. Complexity of finite-variable fragments of propositional modal logics of symmetric frames. Logic Journal of the IGPL, 27(1):60-68, 2019.

[201] Rybakov M., Shkatov D. Undecidability of first-order modal and intuition-istic logics with two variables and one monadic predicate letter. Studia Logica, 107(4):695-717, 2019.

[202] Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages. Journal of Logic and Computation, 30(7):1305-1329, 2020.

[203] Rybakov M., Shkatov D. Recursive enumerability and elementary frame definability in predicate modal logic. Journal of Logic and Computation, 30(2):549-560, 2020.

[204] Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages. Journal of Logic and Computation, 31(5):1266-1288, 2021.

[205] Rybakov M., Shkatov D. Algorithmic properties of first-order superintu-itionistic logics of finite Kripke frames in restricted languages. Journal of Logic and Computation, 31(2):494-522, 2021.

[206] Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with K. Journal of Logic and Computation, 31(2):426-443, 2021.

[207] Rybakov M., Shkatov D. Undecidability of QLTL and QCTL with two variables and one monadic predicate letter. Логические исследования, 27(2):93-120, 2021.

[208] Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with non-transitive modal logics. Journal of Logic and Computation, 32(5):853-870, 2022.

[209] Rybakov M., Shkatov D. Complexity of finite-variable fragments of propo-sitional temporal and modal logics of computation. Theoretical Computer Science, 925:45-60, 2022.

[210] Rybakov M., Shkatov D. Correction to: Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter. Studia Logica, 110:597-598, 2022.

[211] Rybakov M., Shkatov D. Undecidability of the logic of partial quasiary predicates. Logic Journal of the IGPL, 30(3):519-533, 2022.

[212] Rybakov M., Shkatov D. Complexity function and complexity of validity of modal and superintuitionistic propositional logics. Journal of Logic and Computation, 33(7):1566-1595, 2023.

[213] Rybakov M., Shkatov D. Algorithmic properties of modal and superintu-itionistic logics of monadic predicates over finite frames. Journal of Logic and Computation, 35(2):exad078, 2025.

[214] Rybakov M., Shkatov D. Variations on the Kripke trick. Studia Logica, 113:1-48, 2025.

[215] Rybakov M., Shkatov D. Polytime embedding of intuitionistic modal logics into their one-variable fragments. Journal of Logic and Computation (to appear).

[216] Savitch W. J.. Relationships between nondeterministic and deterministic tape complexity. Journal of Computer and System Science, 4:177-192, 1970.

[217] Schewe S. ATL* satisfiability is 2EXPTIME-complete. In: Automata, Languages and Programming. ICALP 2008, volume 5126 of Lecture Notes in Computer Science, pages 373-385, 2008.

[218] Segerberg K. Two-dimensional modal logic. Journal of Philosophical Logic, 2(1):77-96, 1973.

[219] Shapirovsky I. B. Truth-preserving operations on sums of Kripke frames. In: G. Bezhanishvili, G. D'Agostino, G. Metcalfe, and T. Studer, editors, Advances in Modal Logic, 12:541-558. College Publications, 2018.

[220] Shapirovsky I. B. Satisfiability problems on sums of Kripke frames. ACM Transactions on Computational Logic, 23(3):15:1-25, 2022.

[221] Shehtman V., Shkatov D. On one-variable fragments of modal predicate logics. In: Proceedings of SYSMICS2019, pages 129-132. Institute for Logic, Language and Computation, University of Amsterdam, 2019.

[222] Shehtman V., Shkatov D. Some prospects for semiproducts and products of modal logics. In: N. Olivetti and R. Verbrugge, editors, Short Papers Advances in Modal Logic AiML 2020, pages 107-111. University of Helsinki, 2020.

[223] Shehtman V., Shkatov D. Kripke (in)completeness of predicate modal logics with axioms of bounded alternativity. In: First-Order Modal and Temporal Logics: State of the Art and Perspectives (FOMTL 2023), pages 26-29. ESSLLI, 2023.

[224] Shkilniak S. First-order logics of quasiary predicates. Cybernetics and Systems Analysis, 46:884-899, 2010.

[225] Joseph. R. Shoenfield. Degrees of Unsolvability. North-Holland Publishing Company, 1971.

[226] Shoham Y., Leyton-Brown K. Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, 2008.

[227] Sipser M. Introduction to the Theory of Computation. Cengage Learning, 3rd edition, 2013.

[228] Sistla A. P., Clarke E. M. The complexity of propositional linear temporal logics. Journal of ACM, 32(3):733-749, 1985.

[229] Skvortsov D. On axiomatizability of some intermediate predicate logics. Reports on Mathematical Logic, 22:115-116, 1988.

[230] Skvortsov D. On the predicate logic of finite Kripke frames. Studia Logica, 54(1):79-88, 1995.

[231] Skvortsov D. The superintuitionistic predicate logic of finite Kripke frames is not recursively axiomatizable. The Journal of Symbolic Logic, 70(2):451-459, 2005.

[232] Skvortsov D. A remark on superintuitionistic predicate logics of Kripke frames with constant and with nested domains. Journal of Logic and Computation, 21(4):697-713, 2009.

[233] Spaan E. Complexity of Modal Logics. PhD thesis. Department of Mathematics and Computer Science, University of Amsterdam, 1993.

[234] Statman R. Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoret. Comput. Sci., 9(1):67-72, 1979.

[235] Stockmeyer L. J., Meyer A. R. Word problems requiring exponential time: preliminary report. In: Proceedings of the 5th Annual ACM Symposium on Theory of Computing, pages 1-9. ACM, 1973.

[236] Streett R. S. Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54, 1982.

[237] Suranyi J. Zur Reduktion des Entscheidungsproblems des logischen Funk-tioskalktils. Mathematikai es Fizikai Lapok, 50:51-74, 1943.

[238] Svejdar V. The decision problem of provability logic with only one atom. Archive for Mathematical Logic, 42(8):763-768, 2003.

[239] M. Szatkowski. On Fragments of Medvedev's Logic. Studia Logica, 40(1):39-54, 1981.

[240] Takano M. Ordered sets R and Q as bases of Kripke models. Studia Logica, 46:137-148, 1987.

[241] Tarski A., Givant S. A Formalization of Set Theory without Variables, volume 41 of American Mathematical Society Colloquium Publications. American Mathematical Society, 1987.

[242] Turing A. M. On computable numbers, with an application to the 'Entscheidungsproblem'. Proceedings of the London Mathematical Society, 2 series, 42:230-265, 1936/1937.

[243] Urquhart A. Decidability and the finite model property. Journal of Philosophical Logic, 10(3):367-370, 1981.

[244] Urquhart A. The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 49(4):1059-1073, 1984.

[245] Urquhart A. Four variables suffice. The Australasian Journal of Logic, 5, 2007.

[246] Van Benthem J. Modal Logic and Classical Logic. Bibliopolis, 1985.

[247] Van der Hoek W., Wooldridge M. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, 75(1):125-157, 2003.

[248] Van Ditmarsch H., van der Hoek W., Kooi B. Dynamic Epistemic Logic. Springer, 2008.

[249] Vardi M.Y. The taming of converse: Reasoning about two-way computations. In: R. Parikh, editor, Proceedings of the Conference on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 413-424, 1985.

[250] Vardi M. Y., Stockmeyer L. Improved upper and lower bounds for modal logics of programs. In: Proceedings of the seventeenth annual ACM symposium on Theory of computing, pages 240-251, 1985.

[251] Visser A. A propositional logic with explicit fixed points. Studia Logica, 40:155-175, 1981.

[252] Walther D., Lutz C., Wolter F., Wooldridge M. ATL satisfiability is indeed ExpTime-complete. Journal of Logic and Computation, 16(6):765-787, 2006.

[253] Wolter F., Zakharyaschev M. Modal description logics: modalizing roles. Fundamenta Informaticae, 39(4):411-438, 1999.

[254] Wolter F., Zakharyaschev M. Temporalizing description logics. In: D. Gab-bay and M. de Rijke, editors, Frontiers of Combining Systems II, pages 379-401. Studies Press/Wiley, 2000.

[255] Wolter F., Zakharyaschev M. Decidable fragments of first-order modal logics. The Journal of Symbolic Logic, 66:1415-1438, 2001.

[256] Wolter F., Zakharyaschev M. Axiomatizing the monodic fragment of firstorder temporal logic. Annals of Pure and Applied Logic, 118(1-2):133-145, 2002.

[257] Zakharyaschev M., Wolter F., Chagrov A. Advanced Modal Logic. In: D.M.Gabbay, F. Guenthner (editors). Handbook of Philosophical Logic, 3:83-266. Kluwer Academic Publishers, 2nd edition, 2001.

Предметный указатель

агент, 139, 166 аксиомы равенства, 262 алфавит, 23 алгебра

булева, 81 гейтингова, 123 модальная, 81 псевдобулева, 123 алгоритм, 24

с оракулом, 25 арность, 24, 198 буква

предикатная, 198 квазиарная, 382 п-арная,198 п-местная, 198 пропозициональная, 198 валентность, 24, 198 выполнимость глобальная, 397 локальная, 397 высота

шкалы, 233 вхождение переменной свободное, 199 связное, 199

глубина

модальная, 42 шкалы, 233 граф

ациклический, 315 простой, 315 связный, 315 возможность, 36 действие, 167 фиктивное, 167 С-действие, 168 дерево, 315, 316

интранзитивное, 316 иррефлексивное простое, 315 квази-интранзитивное, 316 простое, 316 транзитивное, 316 диагональ множества, 200, 316 дизъюнкция, 30

элементарная, 33 длина формулы, 42 задача

домино, 204, 249, 295 принадлежности, 24 сводимая полиномиально, 28 рекурсивно, 26

С -полная, 26, 29 С -трудная, 26, 29 замыкание

рефлексивно-транзитивное, 177 формула

выполнимая в теории, 201 иерархия

аналитическая, 26 арифметическая, 26 игрок, 166 импликация, 30 индекс

выделенный, 179 индивид, 200 интерпретация

предикатных букв, 200, 221 предметных переменных, 200, 221 иррефлексивизация, 316 истина, 30 история,168 класс

шкал Крипке, 223 первопорядково определимый, 266

с постоянными областями, 223 элементарно определимый, 266 коалиция, 167, 172 композиция, 177 конгруэнтность, 262 конъюнкция, 30

элементарная, 32 корень шкалы Крипке, 38, 130 квантор

всеобщности, 199 первого порядка, 199 пути, 156

существования, 199 лестница Ригера-Нишимуры, 112 литерал, 32 логика

адекватная, 40, 226 дескрипционная, 397 знания, 139

класса шкал, 40, 225, 370 классическая высказываний, 32 конечных моделей, 202 первого порядка, 202 пропозициональная, 32 корректная, 40, 225 локально табличная, 42, 131 модальная, 35 квазинормальная, 63 ненормальная, 64 нормальная, 63, 130 мономодальная, 35 полная по Крипке, 41, 226 предикатная модальная, 219 нормальная модальная, 220 суперинтуиционистская, 351 промежуточная, 87 пропозициональная базисная Виссера, 86 формальная Виссера, 86 интуиционистская, 86

модальная, 38

нормальная модальная, 39, 130 публичных объявлений, 397 сабфреймовая, 42 суперинтуиционистская, 86 табличная, 42, 131 финитно аппроксимируемая, 41, 226 ложь, 30 местность, 198 мир, 36, 128

нормальный, 64 выделенный, 64 взрывающийся, 64 многообразие, 82 множество

неразрешимое, 25 разрешимое, 25

относительно множества, 25 рекурсивно эквивалентное множеству, 25 рекурсивно перечилсимое, 25 рекурсивное, 25 относительно множества, 25 модальность, 24, 35 общего знания, 139 распределённого знания, 139 универсальная, 141 модель

Крипке, 36, 128, 146, 221 интуиционистская, 349 предикатная, 224 пропозициональная, 224

интуиционистская, 85 классическая, 31

классического предикатного языка, 200 конечная, 201 нестандартная, 314 нормальная, 200, 261 параллельных игр, 167 теории, 201 э1Ь-модель, 214 морфизм

псевдоморфизм, 115 р-морфизм, 115 начало пути, 157 начальный отрезок пути, 168 напарник

модальный, 88 предикатный, 220 полный по Крипке, 227 необходимость, 35 номер

гёделев, 26 область

действия квантора, 199 индивидная, 200 предметная, 200 мира, 220 шкалы, 220 оценка, 81, 146, 200, 221 интуиционистская, 85 наследственная, 85 оператор

переименования переменных, 382

оракул, 25 отношение

достижимости, 36, 128, 146, 220 истинности, 31 обратное, 316 э1Ь-отношение, 214 отрицание, 30 переменная

индивидная, 198 предметная, 198 несущественная, 382 существенная, 382 пропозициональная, 23 свободная, 199 перевод

Гёделя, 88, 370 стандартный, 270 плитка домино, 204 подалгебра

порождённая, 82 п-порождённая, 82 подстановка непрямая, 330 прямая, 330 подшкала, 38, 129 корневая, 38,130 порождённая, 38, 130 полупроизведение

¿-полупроизведение логик, 179 шкал, 178 пополнение по Крипке, 227 правило

Гёделя, 39 необходимости, 39 обобщения, 219 подстановки, 38 предикатной подстановки, 219 modus ponens, 39 предикат

частичный квазиарный, 384 предмет, 200 приписывание, 200, 221

частичное, 383 приписывания

неразличимые вне U, 384 существенно неразличимые, 384 программа, 145 произведение логик, 178 шкал, 178 путь, 156, 157, 168 ранг

кванторный, 347 расширение

консервативное, 230 релятивизация, 62, 241 реноминация, 382 символ

кванторный, 198 равенства, 198 следование

семантическое, 269 слияние, 130 сложность, 27

состояние, 146, 156, 157, 167

список

пустой, 199 степень

Тьюринга, 26 неразрешимости, 25 т-степень, 26 Т-степень, 26 стратегия, 168

С-стратегия, 168 сводимость

тьюрингова, 26 т-сводимость, 26 Т-сводимость, 26 связка

логическая, 24 темпоральная, 156 тавтология, 29 теория

конечных моделей, 202 первого порядка, 201

с равенством, 201 предикатных шкал Крипке, 268 терм

программный, 145 атомарный, 145 £-терм, 123 М£-терм, 81 точка, 178

укладка плиток домино, 204, 249, 295 условие

глобально постоянных областей, 221

коммутативности, 178

левой коммутативности, 179 локально постоянных областей, 221

наследственности вверх, 243 вниз, 243 расширяющихся областей, 220 форма

нормальная дизъюнктивная, 32 конъюнктивная, 33 совершенная дизъюнктивная, 32 совершенная конъюнктивная, 33 префиксная, 44 формула

Баркан, 223 атомарная, 31, 199 безымпликативная, 109 выполнимая, 31, 201 замкнтурая, 199 элементарная, 199 монадическая, 245 с равенством, 264 общезначимая, 201 опровержимая, 31, 201 позитивная, 84 предикатная интуиционистская, 349 модальная, 219 пропозициональная интуиционистская, 84 классическая, 32 модальная, 35

пути, 156, 167, 172 состояния, 156, 167, 172 тождественно истинная, 32, 201 тождественно ложная, 32 элементарная, 31 ^-формула, 30, 84 М£-формула, 36 <2£-формула, 200 <2£д-формула, 383 <2£=-формула, 199 <2М£-формула, 219 <2М£=-формула, 263 фрагмент

монадический, 245 с равенством, 264 монодический, 248 позитивный, 84 суперинтуиционистский, 88 функция

перехода, 168 сложности, 67

управления действиями, 168 ширина шкалы, 233 шкала

Крипке, 36, 128, 220 интуиционистская, 349 предикатная, 224 предикатная с равенством, 263 пропозициональная, 224 логики, 40, 225

с предметными областями, 220 Ь-шкала, 40, 225 п-шкала, 177

эквивалентность, 30 язык

классический

первого порядка, 198 предикатный классический, 198 классический с равенством, 198 пропозициональный классический, 32 модальный, 36 полимодальный, 127 £, 30 МС, 36 М£п, 128 ОС, 198, 200 ОС=, 199 219 263