Сложность пропозициональных логик с конечным числом переменных

• Автор: Рыбаков, Михаил Николаевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Тверь
• Количество страниц: 95 с.

1 Необходимые определения
1.1 Синтаксис и семантика
1.2 Классы сложности
2 Основной результат
2.1 Формулировка основного результата
2.2 Модальные логики
2.2.1 Сложность проблемы разрешения в полном языке: вспомогательная конструкция
2.2.2 Сложность константного фрагмента логики К4
2.2.3 Интервал [К, К4]
2.2.4 Сложность фрагмента от одной переменной логики Б4
2.2.5 Интервалы [К4, СЬ] и [К4, Сгг]
2.2.6 Некоторые замечания и следствия
2.3 Базисная и формальная логики Виссера
2.3.1 Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
2.3.2 Сложность проблемы разрешения константного фрагмента логики ВРЬ
2.3.3 Сложность проблемы разрешения фрагмента от одной переменной логики ЕРЬ
2.3.4 Некоторые замечания и следствия

2.4 Суперинтуиционистские логики
2.4.1 Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
2.4.2 Полиномиальное погружение позитивного фрагмента
Int в позитивный фрагмент Int с двумя переменными
2.4.3 Интервал [Int, КС]
2.4.4 Некоторые следствия
2.4.5 Некоторые сложностные аспекты фрагмента от двух переменных логики КС
2.4.6 Обобщения и замечания
3 Анализ полученных результатов
3.1 Функция сложности
3.1.1 К истокам задачи
3.1.2 Оценка функции сложности в случае конечного числа переменных в языке
3.2 Комментарий
Библиография

Актуальность темы. При изучении той или иной логической системы или класса систем исследуются очень разные свойства; круг вопросов, относящихся к алгоритмическим аспектам таких исследований, находится на одном из первых мест. Это объясняется не только чисто теоретическим интересом к алгоритмической выразительности того или иного формального языка, но и возможностью использования полученных результатов в приложениях в информатике, теоретическом программировании и т. д.
В XX веке было получено много результатов, связанных с алгоритмическими свойствами как классических, так и неклассических логик, причём в языках разных порядков и во многих случаях с рядом ограничений на используемые средства этих языков. Опишем ситуацию с интересующими нас аспектами алгоритмической проблематики в отношении пропозициональных логик.
Почти все1 стандартные пропозициональные логики разрешимы (см., например, [5]). Но разрешимость той или иной логики означает лишь наличие принципиальной возможности выяснять факт принадлежности формул этой логике, и когда разрешимость обоснована, встаёт проблема поиска оптимального алгоритма, решающего вопрос о принадлежности формул данной логике. Как правило, из доказательства разрешимости удаётся извлечь лишь такие разрешающие алгоритмы, время работы которых ограничено снизу экспонентой. Естественный вопрос в каждом из таких случаев: а нет ли более быстрого — например, полиномиального по затратам времени — алгоритма разрешения?
1 Исключение составляют, например, релевантные логики, см. [24].

Положим
ТУ* = ТУ и У{И7 : 1 ^ к < п, у, є IV, (ЯЛ, то) и и^п+і : Є ТУ}.
На множестве ТУ* определим отношение Я':
гуД'гу' <=> либо ги, гу' Є ТУ їх гуДгу',
либо гу, гу' Є ТУ,“ и гуД^гу',
либо гу Є ТУ, (ЯЛ, гу) и иі' = (а^+2, гу),
либо и> Є ТУ к ю' — (а"^з, гу).
Пусть Д* — транзитивное замыкание отношения Я'. Положим 5* = (ТУ*, Я*}. Ясно, что 5* — шкала логики ВРЬ.
Пусть ЯЛ* — некоторая модель, определённая на шкале 5*. Покажем, что (ЯЛ, гу0) І£<раДля ВСЯКОЇ! подформулы ф формулы <Р через фа обозначим формулу, получающуюся из ф с помощью подстановки формул ад ап вместо переменных рі,... ,р„.
Покажем, что для всякой подформулы ф формулы (р и для всякого гу Є ТУ имеет место следующая эквивалентность:
(ЯЛ*, гу) |= фа <=> (ЯЛ,гу) (= ф.
Доказательство этого факта проведём индукцией по построению формулы ф.
Для обоснования базиса индукции нам нужно рассмотреть случай, когда Ф
Пусть (ЯЛ, гу) ф'рк- Тогда в шкале 5* из мира ю достижима копия шкалы йк- Нетрудно видеть, что
(ЯЛ*, (акк+2, г»)) И П*+2± -» П^Т,
(ЯЛ*, (а£+2, гу)) ^ (п'г+1± -> □,г±) V □,г+2±,
а поскольку іиЯ*(ак+2,іи), то (ЯЛ*,гу) ¥=ак, т.е. (ЯЛ*,гу) фа.
Пусть (ЯЛ, гу) 1—Рк- Нам нужно показать, что в этом случае (ЯЛ*, гу) |= ак-Предположим, что (ЯЛ*, гу) ^ ак- Тогда для некоторого мира ги' Є ТУ* такого, что гуД*гу' имеют место отношения
(ЯЛ*, гу') (= Ок+2± ->