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

Рыбаков, Михаил Николаевич

Сложность пропозициональных логик с конечным числом переменных тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Рыбаков, Михаил Николаевич АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Тверь МЕСТО ЗАЩИТЫ

2005 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

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

Автореферат диссертации на тему "Сложность пропозициональных логик с конечным числом переменных"

На правах рукописи

Рыбаков Михаил Николаевич

Сложность ПРОПОЗИЦИОНАЛЬНЫХ ЛОГИК С КОНЕЧНЫМ ЧИСЛОМ ПЕРЕМЕННЫХ

01.01.06 - Математическая логика, алгебра в теория чисел

Автореферат диссертации на соискание ученой степени кандидата физико- математических наук

Ярославль - 2005

Работа выполнена в Тверском государственном университете

Научный

руководитель доктор физико-математических наук, профессор

Чагров Александр Васильевич

Официальные

оппоненты доктор физико-математических наук, профессор

Шехтмая Валентин Борисович

кандидат физико-математических наук Яворский Ростислав Эдуардович

Ведущая

организация Красноярский государственный университет

Защита состоится « <// » ЯбЯЩ/Л- 2005 г., в /Г час. .мин. на заседании диссертационного совета Л 212.002.03 при Ярославском государственном университете имени П.Г.Демидова по адресу: г.Ярославль, ул. Союзная, д. 144.

С диссертацией можно ознакомиться в библиотеке Ярославского государственного университета имени П. Г. Демидова.

Автореферат разослав «с/К» 2005 г.

Учёный секретарь

диссертационного совета > с, И. Яблокова

Общая характеристика работы

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

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

Почти все1 стандартные пропозициональные логики разрешимы (см., например, [4]). Но разрешимость той или иной логики означает лишь наличие принципиальной возможности выяснять факт принадлежности формул этой логике, и когда разрешимость обосновала, встаёт проблема поиска оптимального алгоритма, решающего вопрос о принадлежности формул данной логике. Как правило, из доказательства разрешимости удаётся извлечь лишь такие разрешающие алгоритмы, время работы которых ограничено снизу эхспоиен-той. Естественный вопрос в каждом из таких случаев: а нет ли более быстрого — например, полиномиального по затратам времени — алгоритма разрешения?

Одним из первых результатов в этом направлении является теорема Кука: проблема выполнимости булевых формул №-полна [5]. Из теоремы Кука следует, что если Р ф КР, то классическая логика высказываний С] не является полиномиально разрешимой.

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

1 Исключение составляют, например, релевантные логики, см. [17].

сформулированы А.В.Кузнецовым, см. [9]. Одной из проблем, поставленных А. В. Кузнецовым, была проблема полиномиальной эквивалентности интуиционистской логики Int и классической логики С1. Тот факт, что классическая логика сводится полиномиально к интуиционистской, следует из теоремы Гливенко [6]. А.В.Кузнецов показал [22], что если интуиционистская логика является полиномиально аппроксимируемой шкалами Крипке, то она полиномиально сводится к классической, и тем самым эти логики полиномиально эквивалентны. Оставалось лишь обосновать полиномиальную аппроксимируемость интуиционистской логики шкалами Крипке. Как следует из идей, изложенных в [22], ситуация со многими стандартными модальными логиками аналогична.

h(n)= шах min |g|,

Mi«

где 151 — число миров в шкале Крипке а |у>| — длина формулы <р. Результат М. В. Захарьящева состоит в том, что для большого класса неклассических логик, включая интуиционистскую логику, функция сложности ограничена снизу экспоиентой, см. [21], а также [4]. Таким образом, на этом пути решение упомянутого выше вопроса А. В. Кузнецова получить невозможно.

Примерно в это же время Р. Ладнер [10] доказал PSPACE-полноту проблемы разрешения для модальных логик К, Т и S4 и почти сразу Р. Стэтман [14] доказал PSPACE-полноту проблемы разрешения для Int. Таким образом, положительный ответ на вопрос А. В. Кузнецова означал бы, что NP : PSPACE, более того, справедливо и обратное: если NP = PSPACE, то интуиционистская и классическая пропозициональные логики полиномиально эквивалентны.

соответствующая проблема (проблема 18.4):

Легко показать, что Int в языке с одной переменной является линейно аппроксимируемой шкалами Крипке. Является ли Int в языке с двумя переменными линейно (или полиномиально) аппроксимируемой шкалами Крипке? Верно ли, что эта логика полиномиально разрешима? Какова ситуация с S4, Grz и другими стандартными модальными логиками в языке с одной переменной?

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

• Хотя проблема выполнимости булевых формул NP-полна [5], тем не менее, для всякого натурального числа п проблема выполнимости булевых формул от я неременных находится в классе Р. То же верно и для булевых формул с кванторами: проблема выполнимости булевых формул с кванторами (в полном языке) PSPACE-полна (см. [15]), во для любого п проблема выполнимости булевых формул от п переменных с пропозициональными кванторами находится в классе Р. Здесь важно отметить, что для доказательства PSPACE-трудности проблемы разрешения некоторой логики, как правило, к ней проблеме сводят именно эту проблему, и число переменных при таком сведении растёт (как правило, удваивается).

• Аналогичный факт справедлив для всех локально табличных логик: для любого л € N проблема разрешения их фрагментов от п переменных находится в классе Р.

• Проблема выводимости в Int формул от одной переменной находится в классе Р, что следует из конструкции И. Нипшмуры [11].

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

• Как отмечалось выше, доказательства PSPACE-полноты проблемы разрешения неклассических логик были получены в случае языка с бесконечным числом переменных.

• Во второй половине 80-х годов XX века А. В. Чагровым высказывалась гипотеза о том, что интуиционистская логика и многие стандартные модальные логики в языке с конечным числом переменных полиномиально аппроксимируемы шкалами Крипке, в частности, полиномиально разрешимы, причём степень соответствующего полинома зависит от числа переменных в языке2.

• Уже интуиционистский язык с двумя переменными достаточно выразителен: для всякой формулы без отрицания, не выводимой в Int, существует подстановка формул от двух переменных такая, что получающаяся в результате этой подстановки формула тоже не выводится в Int, см. [23]. Кроме того, четырёх переменных достаточно, чтобы построить исчисление с неразрешимым фрагментом от двух переменных [32].

Первые известные диссертанту результаты о PSPACE-трудности проблемы разрешения логик в языке с конечным числом переменных появились в 90-х годах XX века. Так, Дж. Халперн показал [7], что для К, Т, S4 и некоторых полимодальных логик проблема разрешения является PSPACE-полной в языке с одной переменней (к сожалению, работа [7] содержит ошибки в доказательстве для наиболее интересного случая — логики S4). Чуть раньше Э. Спаан доказала [13], что проблема выполнимости модальных формул полиномиально сводится к проблеме выполнимости модальных формул от одной переменной; из этого результата следует, в частности, один из результатов Дж. Халперна, именно, PSPACE-полнота проблемы разрешения фрагмента от одной переменной логике К.

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

Цель работы. Целью работы является выяснение сложности стандартных неклассических (суперинтуиционистских, нормальных модальных и др.) логик в языках с конечным числом переменных. Одной из центральных проблем здесь является упомянутая выше проблема 18.4 [4] и близкие к ней.

2 Эта гипотеза высказывалась на логических конференциях, но не была нигде опуЛлихо аана; А. В. Чагров сообщил диссертанту об этой гипотезе лично, см. также [3].

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

Основные результаты диссертации содержатся в следующей таблице в пунктах 1-2, 6-8, 10-11, 13-14. Факты, указанные в пунктах 3-5, 9, 12, получены не диссертантом (см. [4], [7], [11], [18]) и приведены для полноты описания ситуации.

Номер Логики, Проблема Функция

п.п. п переменных разрешения сложности

1 К,К4,п>0 PSPACE-полна эксп.

2 [К,К4],п>0 PSPACE-трудна ^ ЭКГ.Ц.

3 D, Т, D4, S3, S4,Gra,n—0 находится в Р полином.

4 GL,n = 0 находится в Р полином.

5 Т,п>1 PSPACE-полна эксп.

6 D, D4, S3, S4, Grz, GL, n > 1 PSPACE-полна эксп.

7 [К, GL], [К, вга], [S3, Grss], n > 1 PSPACE-трудна > эксп.

8 BPL, n > 0 PSPACE-полна эксп.

9 FPL,n = 0 находится в Р полином.

10 FPL, n^l PSPACE-полна эксп.

11 [BPL,FPL],n>l PSPACE-трудна > эксп.

12 [Int,KC],nsi 1 находится в Р полином.

13 Int+,Int,KC,n>2 PSPACE-полна эксп.

14 [BPL+,KC+],n>2 PSPACE-трудна ^ эксп.

Запись «эксп.» в графе «Функция сложности» в этой таблице означает, что функция сложности экспоненциальна, запись «> эксп.» — что функция сложности ограничена снизу экспоненциальной фукнцией, «полином.» — что функция сложности полиномиальна.

Обозначения для приведённых в таблице модальных и суперинтуиционистских логик стандартны и соответствуют [4]; через BPL и FPL обозначены базисная и формальная пропозициональные логики Виссера [18].

Научная новизна. Все результаты диссертации являются новыми.

Работами, в которых представлены близкие результаты, являются [7], [13] и [16]. Результат [13] касается только логики К, точнее, её фрагмента от одной переменной. В [7] рассматриваются модальные логики К, Т и S4 в случае одной переменной и отсутствия в языке логических констант. При этом в диссертации усилен результат [7] и [13], касающийся логики К. Это усиление состоит в том, что при наличии в языке логической константы -L доказана PSPACE-полнота проблемы разрешения константного фрагмента логики К. Дано корректное доказательство утверждения [7] в случае логики S4. В [16] рассматривается только логика Гёделя-Лёба3. Полученные в [7], [13] и [16] результаты в отношении указанных логик являются следствиями результатов данной диссертации.

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

Апробация. Результаты работы докладывались на международных конференциях «Advances in Modal Logic» (Франция, Тулуза, 2002 г.), «Колмогоров и современная математика» (Москва, 2003 г.), «Смирновские чтения» (Москва, 2003 г.), «Современная логика: Проблемы теории, истории и применения в науке» (Санкт-Петербург, 2002 г. и 2004г.), «Computer Science Applications of Modal Logic» (Москва, 2005г.). Кроме того, результаты, вошедшие в диссертацию, докладывались на семинаре по неклассической логике в МГУ (руководитель семинара — проф. В.Б.Шехтман), на семинаре по математической логике Тверского госуниверситета (руководитель —■ проф. А. В.Чагров), на семинаре по информационным процессам в МГУ (руководитель — проф. В. А.Любецкий), на научно-исследовательском семинаре логического центра Института философии РАН (руководитель — проф. А.С.Карпенко), на научном семинаре в секторе логики Института философии РАН (руководитель — проф. А. С. Карпенко).

3В [16] имеете« ссылка и» работу диссертанта [2] (в соавторстве с А. В. Чагровьш), причем в [2] среди прочих содержится и результат [16]; но в [16] автор отмечает, что его результат получен в 1998 году.

*Си., налриыер, [24].

Публикации. Основные результаты диссертации опубликованы в [2], [3], [12], [20], [25], [26], [27], [28], [29], [30].

Структура я объвм работы. Диссертация состоит из введения, трёх глав и библиографического списка, включающего 45 наименований. Объём » работы — 95 стр.

Содержание работы

Во введении обосновывается актуальность темы диссертации, формулируется цель работы, описываются методы проведения исследования. Описываются основные результаты работы и даётся обзор всех разделов диссертации.

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

Глава 2 посвящена решению проблемы 18-4, поставленной в [4].

Для формулировки основного результата главы 2 введём следующие обозначения. Для пропозициональной логики Ь и натурального числа п через £(п) обозначим фрагмент логики £, состоящий из формул в языке, содержащем ровно п пропозициональных переменных. Кроме того, для логики (множества формул) £ в интуиционистском языке через £+ обозначим позитивный фрагмент £, т. е. множество формул из £, построенных из пропозициональных переменных с помощью Л, V и -4.

Основной результат главы 2 представлен в следующих утверждениях8.

Теорема 2.1. Пусть логика £ находится в одном из следующих интервалов: [К(0),К4(0)], [К(1),ОЬ(1)], [К(1),вгв(1)], [ВРЬ(1),ИРЬ(1)], [ВРЬ+ (2), КС+ (2)]. Тогда проблема разрешения для £ является РЭРАСЕ-< трудной.

'Результат, касающийся интуициоинсткой логики и еб расширений содержит ответ на вопрос, доставленный в [20].

Теорема 2.2. Пусть L — одна из следующих логик: К(0), К4(0), BPL(O), D(l), D4(l), T(l), S4(l), GL(1), Gra(l), FPL(1}, Int+(2), KC(2). Тогда проблема разрешения для L является PSPACE-полкой.

Доказательство этих теорем изложено в разделах 2.2, 2.3 и 2.4. В разделе 2.2 рассматриваются стандартные модальные логики с PSPACE-полной проблемой разрешения в полном языке. В разделе 2.3 рассматривается базисная логика Виссера и её расширения, в частности, формальная логика Вис-сера [18]. В разделе 2.4 рассматривается интуиционистская логика, а также промежуточные логики, содержащиеся в логике слабого закона исключённого третьего.

В каждом из этих разделов сначала (соответственно, в подразделах 2.2.1, 2.3,1 и 2.4.1) описывается конструкция, позволяющая обосновать PSPACE-трудность проблемы разрешения соответствующих логик в полном языке, при этом используются идеи, близкие изложенным в [10] и [14]. Именно, к рассматриваемой проблеме сводится проблема выполнимости булевых формул с кванторами, которая, как известно, PSPACE-полна [15]. Возникающие при этом формулы имеют незначительные для доказательства PSPACE-трудности отличия от формул, предложенных в [10] и [14]. Эти формулы будут служить основой для дальнейших модификаций, проводимых с целью получения основных результатов главы 2, и соответствующие отличия сыграют свою (техническую) роль.

В подразделе 2.2.2 разрабатывается основная конструкция, позволяющая доказать PSPACE-трудность проблемы разрешения константного фрагмента логики К4. В подразделе 2.2.3 производится незначительная модификация этой конструкции, и обосновывается PSPACE-трудность проблемы разрешения константных фрагментов логик из интервала [К, К4].

В подразделе 2.2.4 показано, что константные фрагменты расширений логики S4 полиномиально разрешимы. Далее рассматривается вопрос о сложности проблемы разрешения S4 в языке с одной переменной. Описывается, в чём состоит некорректность доказательства PSPACE-трудности этой проблемы в [7], и приводится корректное доказательство. Модификации конструкции, возникающей в ходе этого доказательства, позволяют обосновать PSPACE-трудность проблемы разрешения фрагментов от одной переменной для логик из интервалов [К, QL] и [К, Grz]. Соответствующие доказательства приводятся в подразделах 2.2.5 и 2.2.6.

В подразделах 2.3.2 и 2.3.3 доказывается, соответственно, PSPACE-

полнота проблемы разрешения константного фрагмента базисной логики Вис-сера BPL и фрагмента от одной переменной формальной логики Виссе-ра FPL. При этом используется техника, аналогичная применённой в разделе 2.2 для модальных логик К4 и GL. В подразделе 2.3.4 доказывается PSPACE-трудность проблемы разрешения фрагментов от одной переменной логик из интервала [BPL,FPL].

Так как фрагменты суперинтуиционистских логик от одной переменной полиномиально разрешимы, то описанные ранее конструкции для языков без переменных и с одной переменной в случае интуиционистской логики применить невозможно. Для случая двух переменных в языке в подразделе 2.4.2 разрабатывается новая конструкция, с помощью которой доказывается PSPACE-трудность проблемы разрешения позитивного фрагмента Int. В подразделе 2.4.3 доказывается PSPACE-трудность проблемы разрешения фрагментов от двух переменных логик из интервала [Int, КС]. Некоторые следствия из последнего факта представлены в подразделе 2.4.4. Именно, показано, что следующие логики обладают PSPACE-трудной проблемой разрешения в языке с двумя переменными:

• все непротиворечивые отличные от С1 логики, аксиоматизируемые над Int формулой от одной переменней;

• все непротиворечивые отличные от С1 логики, аксиоматизируемые над Int безымпликативной формулой;

• логика Крайэеля-Патнэма KP, логика Медведева ML, а также все логики из интервала [KP, ML].

В подразделе 2.4.5 в качестве следствия из разработанной конструкции получено усиление одного из результатов С. И. Мардаева [23]. Именно, доказано, что для всякой не принадлежащей КС формулы существует подстановка формул от двух переменных, удлиняющая исходную формулу полиномиально и такая, что получившаяся формула тоже не принадлежит логике КС, при этом задача нахождения такой подстановки является NP-трудной.

Ещё одно следствие представлено в подразделе 2.4.6: доказано, что позитивный фрагмент от двух переменных всякой логики из интервала [BPL, КС] обладает PSPACE-трудной проблемой разрешения. Также доказано, что в случае позитивного фрагмента базисной пропозициональной логики Виссера PSPACE-трудна уже проблема разрешения для BPL+(1).

В главе 3 обсуждается связь полученных в главе 2 результатов с близкими (в том числе открытыми) вопросами.

В разделе 3.1 рассматривается функция сложности [4] для фрагментов логик, о которых говорится в теоремах 2.1 и 2.2. Описывается связь между сложностью6 этой функции и проблемой полиномиальной сводимости Int и других стандартных пропозициональных логик к классической логике С1. Именно, если функция сложности доя одной из рассматриваемых логик полиномиальна, то эта логика полиномиально сводима к С1 (см. также [22]); из последнего, в частности, следует сомнительное равенство классов NP и PSPACE. Здесь же представлены основные результаты главы 3. Для их формулировки нам потребуется следующее определение.

Фуакцшо f(n) будем называть экспоненциальной, если существуют положительные числа ai,bi,a¡, Ь^ такие, что для всякого п, большего некоторого по,

2"1 < /(п)< 2°* .

ТЕОРЕМА 3.1. Пусть логика L находится в одном из следующих интервалов: [К(0),К4(0)], [K(1),GL(1)], [K(l),Grz(l)], [BPL(1),FPL(1)], [BPL+(2),KC+(2)]. Тогда функция /¿(п) ограничена снизу некоторой экспоненциальной функцией.

Теорема 3.2. Пусть L — одна из следующих логик: К(0), К4(0), BPL(O), D(l), D4(l), T(l), S4(l), GL(1), Gr«(l), FPL(l), Int+(2), KC(2). Тогда функция /¿(n) является экспоненциальной.

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

В разделе 3.2 даётся комментарий полученным результатам. Указаны некоторые вопросы, возникающие ввиду теорем 2.1 и 2.2. Приводятся примеры применения разработанной техники для получения аналогичных результатов для логик из других классов. Так, с помощью этой техники в [3] доказано, что проблема выполнимости для GLLin(l), S4.3(l), Grz.3(2) является NP-полной. Показано, что описанная техника работает и в случае ненормальных (квазинормальных) модальных логик. В качестве примера рассматривается медальная логика S3, которая, в отличие от рассмотренных в главе 2 модальных логик, не замкнута относительно правила Гбделя. Доказывается, что

'Имеется в виду порядок функции, причём в смысле довольно грубой опенки: поляной, экспонента н т. п.

проблема разрешения фрагмента от одной переменной логики S3 является

PSPACE-полной, а функция сложности — экспоненциальной.

Литература

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

[2] A. V.Chagrov, M.N.Rybakov. Least Number of Vanables for PSPACE-Hardness of Provability Problem m Systems of Modal Logic // Advances in Modal Logic. 30 Septembre - 2 Octobre 2002. Institut de Reacherche en Informatique de Toulouse, Université Paul Sabatier, Toulouse, Prance, 2002, p. 178-188.

[3] A.V.Chagrov, M.N.Rybakov. How Many Variables One Needs to Prove PSPACE-Hardness of Modal Logics? // Advances in Modal Logic, vol. 4, London, King's College Publications, 2003, p. 71-82.

[4] A. V. Chagrov, M. V. Zakharyascbev. Modal Logic. Oxford University Press, 1997.

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

[6] V. Glivenko. Sur quelques points de la logique de M. Brouwer // Bulletin de la Classe des Sciences de l'Académie Royale de Belgique, vol. 15, 1929, p. 183-188.

[7] J. Y. Halpern. The Effect of Bounding the Number of Primitive Propositions and the Depth of Nesting on the Complexity of Modal Logic 11 Artificial Intelligence, vol. 75, No. 2,1995, p. 361-372.

[8] J. Y. Halpern, Y. Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief // Artificial Intelligence, 1992, vol. 54, p. 319379.

[9] A. V. Kuznetsov. On Superintuitiontstic Logics // Proceedings of the International Congress of Mathematicians, Vancouver, 1975, p. 243-249.

[10] R. E. Ladner. The Computational Complexity of Provability in Systems of Modal Logic // SIAM Journal on Computing, vol.6, 1977, p. 467-480.

[11] I. Nishimura. On Formulas of the One Variable in Intuitionistic Prepositional Calculus // The Journal of Symbolic Logic, vol. 25, No. 1, 1960, p. 327-331.

[12] MN.Rybakov. Complexity of the Two-Variable Fragment of Intuitionistic Proposition^ Logic // Computer Science Applications of Modal Logic. International Conference. September 5-9 2005. Moscow, Poncelet Laboratory of UMI 2615 and Independent University of Moscow, 2005, p. 35-36.

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

[14] R. Statman. Intuitionistic Proposittonal Logic is Polynomial-Space Complete Ц Theoret. Comput. Sci., vol.9, No.l, 1979, p.67-72.

[15] L.Stockmeyer. Classifying the Computational Complexity of Problems // The Journal of Symbolic Logic, vol. 52, No. 1, 1987, p. 1-43.

[16] V. Svejdar. The Decision Problem of Provability Logic with Only One Atom II Arch. Math. Logic, 2003, p. 1-6.

[17] A. Urquhart. The Undecidability of Entailment and Relevant Implication // The Journal of Symbolic Logic, vol.49, No. 4, 1984, p. 1059-1073.

[18] A. Visser. A Proposittonal Logic with ExpHctt Fixed Points // Studia Logica, vol.40, 1981, p. 155-175.

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

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

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

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

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

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

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

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

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

[28] М.Н.Рыбаков, А.В.Чагров. Модальные формулы без переменных и РЯРАСЕ-полнота // Современная логика: Проблемы теории, истории и применения в науке. Материалы VII Международной научной конференции. СПб, Издательство Санкт-Петербургского университета, 2002, с. 498-500.

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

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

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

[32] А. В. Чагров. Неразрешимые свойства суперинтуиционистских логик // Математические вопросы кибернетики, вып. 5. М., Физмат лит, 1994, с. 62-108.

р24 9 1 л

РНБ Русский фонд

2006-4 '

27345

Содержание диссертации автор исследовательской работы: кандидата физико-математических наук, Рыбаков, Михаил Николаевич

Введение

1 Необходимые определения

1.1 Синтаксис и семантика.

1.2 Классы сложности.

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

2.1 Формулировка основного результата.

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

2.2.1 Сложность проблемы разрешения в полном языке: вспомогательная конструкция.

2.2.2 Сложность константного фрагмента логики К

2.2.3 Интервал [К, К4].

2.2.4 Сложность фрагмента от одной переменной логики S

2.2.5 Интервалы [К4, GL] и [К4, Grz].

2.2.6 Некоторые замечания и следствия

2.3 Базисная и формальная логики Виссера.

2.3.1 Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция.

2.3.2 Сложность проблемы разрешения константного фрагмента логики BPL.

2.3.3 Сложность проблемы разрешения фрагмента от одной переменной логики FPL.

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 Комментарий.

Введение диссертация по математике, на тему "Сложность пропозициональных логик с конечным числом переменных"

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

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

1 Исключение составляют, например, релевантные логики, см. [24].

Одним из первых результатов в этом направлении является теорема Кука: проблема выполнимости булевых формул NP-полна [6]. Из теоремы Кука следует, что если Р ф NP, то классическая логика высказываний не является полиномиально разрешимой.

Хотя для многих стандартных логик оценки для верхних границ размера контрмоделей были получены довольно давно, предметом специальных исследований сложность неклассических логик стала только в конце XX века. Дело в том, что получение таких оценок являлось, как правило, лишь промежуточным этапом на пути доказательства разрешимости соответствующих логик, и вопросы сложности при этом не рассматривались. Вопросы о сложности неклассических (точнее, суперинтуиционистских) логик впервые были явно сформулированы А.В.Кузнецовым, см. [13]. Одной из проблем, поставленных А. В. Кузнецовым, была проблема полиномиальной эквивалентности интуиционистской и классической логик. Тот факт, что классическая логика сводится полиномиально к интуиционистской, следует из теоремы Гливенко [9]. А.В.Кузнецов показал [32], что если интуиционистская логика является полиномиально аппроксимируемой шкалами Крипке, то она полиномиально сводится к классической, и тем самым эти логики полиномиально эквивалентны. Как следует из идей, изложенных в [32], ситуация со многими стандартными модальными логиками аналогична. Оставалось лишь обосновать полиномиальную аппроксимируемость интуиционистской логики шкалами Крипке.

Вопрос о полиномиальной аппроксимируемости интуиционистской логики шкалами Крипке был решён в конце 70-х годов XX века М. В. Захарьящевым. В своих работах М. В. Захарьящев рассматривал следующую функцию сложности fb(n), определяемую для логики L: ь(п) — max min где Ul — число миров в шкале Крипке а — длина формулы (р. Результат М. В. Захарьящева состоит в том, что для большого класса неклассических логик, включая интуиционистскую логику, функция сложности ограничена снизу экспонентой, см. [31], а также [5]. Таким образом, на этом пути решение упомянутого выше вопроса А. В.Кузнецова получить невозможно.

Примерно в это же время Р.Ладнер [14] доказал PSPACE-полноту проблемы разрешения для модальных логик К, Т и S4 и почти сразу Р. Стэтман [20] доказал PSPACE-полноту проблемы разрешения для Int. Таким образом, положительный ответ на вопрос А.В.Кузнецова означал бы, что NP = PSPACE, более того, справедливо и обратное: если NP = PSPACE, то интуиционистская и классическая пропозициональные логики полиномиально эквивалентны.

Как Р. Ладнер, так и Р. Стэтман использовали в доказательствах PSPACE-полноты формулы в языках, содержащих бесконечно много переменных; то же можно сказать и об опубликованных позже доказательствах PSPACE-трудности проблемы разрешения тех или иных логик (см., например, [1], [5], [11], [27], [43]). Тем не менее, прикладные задачи не требуют неограниченного числа переменных в языке: как при постановке, так и при решении каждой прикладной задачи используется лишь конечное число элементарных выражений, для описания которых достаточно, конечно же, конечного числа переменных. Более того, даже язык без переменных представляет определённый интерес: поскольку формулы являются лишь схемами высказываний, то, решив ту или иную проблему для логики в целом, разумно посмотреть, как это решение соотносится со множеством самих высказываний, а типичными высказываниями можно считать как раз константные формулы. Таким образом, вполне естественно рассматривать фрагменты логик в языке с конечным числом переменных, и в [5] сформулирована соответствующая проблема (проблема 18.4):

• Хотя проблема выполнимости булевых формул NP-полна [6], тем не менее, для всякого натурального числа п проблема выполнимости булевых формул от п переменных находится в классе Р. То же верно и для булевых формул с кванторами: проблема выполнимости булевых формул с кванторами (в полном языке) PSPACE-полна (см. [21]), но для любого п проблема выполнимости булевых формул с кванторами от п переменных находится в классе Р.

• Аналогичный факт справедлив для всех локально табличных логик2: проблема разрешения их фрагментов в языке от п переменных находится в классе Р.

• Проблема выводимости в Int формул от одной переменной находится в классе Р, что следует из конструкции И. Нишимуры [15].

• Как отмечалось выше, доказательства PSPACE-полноты проблемы разрешения неклассических логик были получены в случае языка с бесконечным числом переменных; то же относится к упомянутым результатам М. В. Захарьящева. При этом для любого п фрагменты соответствующих логик, состоящие из формул от не более чем тг переменных, использовавшихся Р. Ладнером и Р. Стэтманом для обоснования PSPACE-трудности, полиномиально разрешимы, поскольку они моделируют в этих логиках проблему выполнимости булевых формул с кванторами в языке с конечным числом переменных. Более того, в доказательстве Р. Стэтмана PSPACE-полноты проблемы разрешения Int использовались лишь связки А и —а проблема разрешения соответствующего фрагмента Int в языке с конечным числом переменных находится в классе Р.

2Формулы <р и ф эквивалентны в L, если ip О ф 6 L. Нормальная модальная или суперинтуиционистская логика L называется локально табличной, если для каждого тг £ N имеется лишь конечное число попарно неэквивалентных в L формул от переменных РЪ

• Примерно во второй половине 80-х годов XX века А. В. Чагровым высказывалась гипотеза о том, что интуиционистская логика и стандартные модальные логики в языке с конечным числом переменных полиномиально аппроксимируемы шкалами Крипке, в частности, полиномиально разрешимы, причём степень соответствующего полинома зависит от числа переменных в языке3.

• Уже интуиционистский язык с двумя переменными достаточно выразителен: для всякой формулы без отрицания, не выводимой в Int, существует подстановка формул от двух переменных такая, что получающаяся в результате этой подстановки формула тоже не выводится в Int, см. [34]. Кроме того, четырёх переменных достаточно, чтобы построить исчисление с неразрешимым фрагментом от двух переменных [44].

Первые известные диссертанту результаты о PSPACE-трудности проблемы разрешения логик в языке с конечным числом переменных появились лишь в 90-х годах XX века. Так, Дж. Халперн показал [10], что для К, Т, S4 и некоторых полимодальных логик проблема разрешения является PSPACE-полной в языке с одной переменной (к сожалению, работа [10] содержит ошибки в доказательстве для наиболее интересного случая — логики S4). Чуть раньше Э. Спаан доказала [19], что проблема выполнимости модальных формул полиномиально сводится к проблеме выполнимости модальных формул от одной переменной; из этого результата следует, в частности, один из результатов Дж. Халперна, именно, PSPACE-полнота проблемы разрешения фрагмента от одной переменной логики К.

3Эта гипотеза высказывалась на логических конференциях, но не была нигде опубликована; А. В.Чагров сообщил диссертанту об этой гипотезе лично, см. также [4].

Основные результаты диссертации представлены в следующей таблице.

Логики, п переменных Проблема разрешения Функция сложности

К,К4,п^0 PSPACE-полна, [0] эксп., [0]

К,К4],п^0 PSPACE-трудна, [0] ^ эксп., [0]

D, Т, D4, S3, S4, Grz,n = 0 находится в Р, (т) полином., (т)

GL, n = 0 находится в Р, см. [5] полином., см. [5]

T.n^l PSPACE-полна, [10], [0] эксп., [0], сл. [10]

D, D4, S3, S4, Grz, GL, n ^ 1 PSPACE-полна, [0] эксп., [0]

K, GL], [K, Grz], [S3, Grz], n ^ 1 PSPACE-трудна, [0] ^ эксп., [0]

BPL,n^0 PSPACE-полна, [0] эксп., [0]

FPL,n = 0 находится в Р, сл. [26] полином., сл. [26]

FPL, n ^ 1 PSPACE-полна, [0] эксп., [0]

BPL, FPL], n ^ 1 PSPACE-трудна, [0] ^ эксп., [0]

Int,KC],n^l находится в Р, сл. [15] полином., [15]

Int+,Int,KC,n^2 PSPACE-полна, [0] эксп., [0]

BPL+,KC+],n>2 PSPACE-трудна, [0] ^ эксп., [0]

Ссылка [0] в этой таблице означает, что соответствующий результат получен в данной диссертации, пометка (т) означает, что соответствующий факт тривиален. Сокращение «сл.» означает «следует из». Запись «эксп.» в графе «Функция сложности» означает, что функция сложности экспоненциальна, запись эксп.» — что функция сложности ограничена снизу экспоненциальной фукнцией, «полином.» — что функция сложности полиномиальна.

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

Научная новизна. Все результаты диссертации являются новыми.

Работами, в которых представлены близкие результаты, являются [10], [19] и [22]. Результат [19] касается только логики К, точнее, её фрагмента от одной переменной. В [10] рассматриваются модальные логики К, Т и S4 в случае одной переменной и отсутствия в языке логических констант. При этом в диссертации усилен результат [10] и [19], касающийся логики К. Это усиление состоит в том, что при наличии в языке логической константы L доказана PSPACE-полнота проблемы разрешения константного фрагмента логики К. Дано корректное доказательство утверждения [10] в случае логики S4. В [22] рассматривается только логика Гёделя-Лёба4. Полученные в [10], [19] и [22] результаты в отношении указанных логик являются следствиями результатов данной диссертации.

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

4В [22] имеется ссылка на работу автора [3] (в соавторстве с А. В. Чагровым), причём в [3] среди прочих содержится и результат [22]; но в [22] автор отмечает, что его результат получен в 1998 году.

5См., например, [36]. и применения в науке» (Санкт-Петербург, 2002 г. и 2004 г.), «Computer Science Applications of Modal Logic» (Москва, 2005 г.). Кроме того, результаты, вошедшие в диссертацию, докладывались на семинаре по неклассической логике в МГУ (руководитель семинара — проф. В. Б. Шехтман), на семинаре по математической логике Тверского госуниверситета (руководитель — проф. А. В.Чагров), на семинаре по информационным процессам в МГУ (руководитель — проф. В. А. Любецкий), на научно-исследовательском семинаре логического центра Института философии РАН (руководитель — проф. А.С.Карпенко), на научном семинаре в секторе логики Института философии РАН (руководитель — проф. А. С. Карпенко).

Публикации. Основные результаты диссертации опубликованы в [3], [4], [17], [28], [37], [38], [39], [40], [41], [42].

Структура и объём работы. Диссертация состоит из введения, трёх глав и библиографического списка, включающего 45 наименований. Объём работы — 95 стр.

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Рыбаков, Михаил Николаевич, Тверь

1. P. Blackburn, M. de Rijke, Y. Venema. Modal Logic. Cambridge University-Press, 2001.

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

3. A. V. Chagrov, M. N. Rybakov. How Many Variables One Needs to Prove PSPACE-Hardness of Modal Logics? // Advances in Modal Logic, vol.4, London, King's College Publications, 2003, p. 71-82.

4. A. V. Chagrov, M. V. Zakharyaschev. Modal Logic. Oxford University Press, 1997.

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

6. D. M. Gabbay. The Decidability of the Kreisel-Putnam System // The Journal of Symbolic Logic, vol.35, No.3, Sept. 1970, p. 431-437.

7. M. R. Garey, D. S. Johnson. Computers and Intractability, A Guide to the Theory of NP-completeness. San Francisco, 1979.

8. V. Glivenko. Sur quelques points de la logique de M. Brouwer // Bulletin de la Classe des Sciences de l'Academie Royale de Belgique, vol. 15, 1929, p.183-188.

9. J. Y. Halpern. The Effect of Bounding the Number of Primitive Propositions and the Depth of Nesting on the Complexity of Modal Logic // Artificial Intelligence, vol. 75, No. 2, 1995, p. 361-372.

10. J.Y.Halpern, Y.Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief // Artificial Intelligence, 1992, vol. 54, p. 319-379.

11. N.Immerman. Descriptive Complexity. Springer, 1999.

12. A. V. Kuznetsov. On Superintuitionistic Logics // Proceedings of the International Congress of Mathematicians, Vancouver, 1975, p. 243-249.

13. R. E. Ladner. The Computational Complexity of Provability in Systems of Modal Logic // SIAM Journal on Computing, vol.6, 1977, p.467-480.

14. I. Nishimura. On Formulas of the One Variable in Intuitionistic Propositional Calculus // The Journal of Symbolic Logic, vol.25, No. 1, 1960, p. 327-331.

15. С. H. Papadimitriou. Computational Complexity. Addison-Wesley Publishing Company, 1995.

16. W. J. Savitch. Relationships Between Nondeterministic and Deterministic Tape Complexity // Journal of Computer and System Science, vol. 4, 1970, p.177-192.

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

18. R. Statman. Intuitionistic Propositional Logic is Polynomial-Space Complete // Theoret. Comput. Sci., vol.9, No. 1, 1979, p.67-72.

19. L. Stockmeyer. Classifying the Computational Complexity of Problems // The Journal of Symbolic Logic, vol. 52, No. 1, 1987, p. 1-43.

20. V. Svejdar. The Decision Problem of Provability Logic with Only One Atom // Arch. Math. Logic, 2003, p. 1-6.

21. M. Szatkowski. On Fragments of Medvedev's Logic // Studia Logica, vol. 40, No. 1, 1981, p. 39-54.

22. A. Urquhart. The Undecidability of Entailment and Relevant Implication // The Journal of Symbolic Logic, vol.49, No.4, 1984, p. 1059-1073.

23. A. Urquhart. The Complexity of Propositional Proofs // The Bulletin of Symbolic Logic, vol.1, No. 4, Dec. 1995, p. 425-466.

24. A. Visser. A Propositional Logic with Explicit Fixed Points // Studia Logica, vol.40, 1981, p. 155-175.

25. M. Zakharyaschev, F. Wolter, and A. Chagrov. Advanced Modal Logic // D.M. Gabbay, F. Guenthner (editors). Handbook of Philosophical Logic, vol.3, p.83-266. Kluwer Academic Publishers, 2nd edition, 2001.

26. М. Гэри, Д. Джонсон. Вычислительные машины и труднорешаемые задачи. М., Мир, 1982.

27. Ю.Л.Ершов, Е.А.Палютин. Математическая логика. Изд. 2-е. М., Наука, 1987.• 31. М. В. Захарьящев, С.В.Попов. О мощности контрмоделей интуиционистского исчисления // Препринт ИПИ АН СССР, N45, 1980.

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

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

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

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

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

33. М. Н. Рыбаков. Сложность проблемы разрешения базисной и формальной логик // Логические исследования, вып. 10. М., Наука, 2003, с. 158166.

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

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

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

37. M. H. Рыбаков, А. В. Чагров. О сложности модальных логик, имеющих доказуемостную интерпретацию, с ограничениями на число переменных // Колмогоров и современная математика. Международная конференция. М., Издательство МГУ, 2003, с. 707-708.

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

39. А. В. Чагров. Неразрешимые свойства суперинтуиционистских логик // Математические вопросы кибернетики, вып. 5. М., Физматлит, 1994, с. 62-108.

40. В. А. Янков. Об исчислении слабого закона исключённого третьего // Известия АН СССР. Сер. матем., т. 2, N5, 1968, с. 1044-1051.i