Введение
1 Основные определения 14
1.1 Итеративные операторы: синтаксис и семантика 14
1.2 Разрешимость и сложность 17
2 О разрешимости теорий с итеративными операторами 19
2.1 О разрешимости теории с транзитивным замыканием по одной паре переменных 19
2.1.1 Формулы с равенствами 19
2.1.2 Предикаты делимости 25
2.1.3 Звенья разных знаков 32
2.1.4 Неравенства 37
2.1.5 Внешние ограничения 45
2.2 О неразрешимости арифметики Пресбургера и арифметики Ско лема с оператором транзитивного замыкания 60
2.2.1 Арифметика Пресбургера 60
2.2.2 Арифметика Сколема 61
2.3 О разрешимости теории с оператором наименьшей фиксированной точки 66
2.3.1 Экзистенциальные формулы с равенствами 66
2.3.2 Шаблоны разных знаков 74
2.3.3 Предикаты делимости 77
2.3.4 О фиксированной точке для двух кластеров 79
2.3.5 О вложенном операторе наименьшей фиксированной точки 90
2.4 Об одноместном операторе инфляционной фиксированной точки 117
3 Оценки сложности разрешающих алгоритмов для теории с FP оператором 122
3.1 О временой сложности разрешающего алгоритма для теории с оператором наименьшей фиксированной точки 123
3.2 О нижней границе временной сложности разрешающих алгоритмов для теории с оператором наименьшей фиксированной точки
3.2.1 Об экспоненциальном сдвиге 129
3.2.2 О моделировании клеточных автоматов 132
3.2.3 Об экспоненциальном сдвиге посредством экзистенциальных формул 140
Заключение 144
Литература
