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

• Рыбаков, Михаил Николаевич
• кандидат физико-математических наук
• 2005

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

Введение

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

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

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

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

Почти все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):

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

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

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

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

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

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

• Как отмечалось выше, доказательства 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].

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

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

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

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

К,К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, а также в преподавании разделов математической логики, связанных с приложениями в теоретическом программировании, информатике и т. д.

Апробация. Результаты работы докладывались на международных конференциях «Advances in Modal Logic» (Франция, Тулуза, 2002 г.), «Колмогоров и современная математика» (Москва, 2003 г.), «Смирновские чтения» (Москва, 2003 г.), «Современная логика: Проблемы теории, истории

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 стр.

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

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