-2-
Огл явление
Введение 5
Полуалгебраические системы доказательств....................... 7
Статические полуалгебраические системы доказательств 8
Полуалгебраические системы доказательств гснценовского типа . 9
Полуалгебраические системы с ограниченной степенью ложности 10 Структура диссертации...................................... 11
1 Используемые системы доказательств и семейства тавтологий 15
1.1 Пропозициональные системы доказательств.................. 17
1.2 Алгебраические системы доказательств..................... 19
1.3 Полуалгебраические системы доказательств ................ 21
1.4 Статические полуалгебраические системы доказательств . . 24
1.5 Полуалгебраические системы доказательств гснценовского
типа..................................................... 25
1.6 Понятие степени ложности................................. 26
1.7 Понятия и обозначения теории графов...................... 27
1.8 Формулы, кодирующие принцип Дирихле...................... 28
1.9 Формулы, кодирующие принцип нераскрашиваемости графа, содержащего клику......................................... 29
1.10 Цейтинекие формулы на графах-расширителях................ 31
2 Сложность статических полуалгебраических систем 35
2.1 Короткое статическое доказательство тавтологии о нераскрашиваемости графа, содержащего клику........................ 35
-3-
2.2 Нижние экспоненциальные оценки на длину вывода цейт-инских формул в статической полуалгебраической системе доказательств Ловаса-Схрайвера............................... 38
2.2.1 Процедура очищения расширителей........................ 38
2.2.2 Линейная нижняя оценка на булеву степень вывода биномиальных цейтииских формул в системе доказательств РБ . 40
2.2.3 Нижние оценки па булеву степень РБ-доказательства биномиальных цейтииских формул................................... 45
2.2.4 Преобразование доказательства цейтииских формул в статической ЬБ+ в доказательство в РБ............................47
2.2.5 Нижняя экспоненциальная оценка на размер доказательства в статической ЬБ+ ...................................... 52
3 Сложность полуалгебраических систем генценовского типа 58
3.1 Полиномиальная эквивалентность Я(Ь&Р) и Я(ЬР), связь ЩСР) и Я(ЬР)................................................. 58
3.2 Полиномиальное моделирование в СР1........................60
3.3 Доказательство полиномиального размера цейтииских формул в ЩЬР)................................................... 61
3.4 Вещественная коммуникационная сложность и нижние экспоненциальные оценки для Я(СР).............................68
4 Сложность полуалгебраических систем с ограниченной степенью ложности 79
4.1 Верхние полиномиальные оценки на размер доказательств принципа Дирихле и принципа иераскрашиваемости графа, содержащего клику............................................ 79
4.2 Полиномиальное моделирование ЬБ*+СР с ограниченной степенью ложности в 11е8(А;)................................. 83
Нижние экспоненциальные оценки для ЬЭ^+СР* с линейной от количества переменных степенью ложности.............
Введение
Необходимость математического изучения понятия доказательства была сформулирована и обоснована Д. Гильбертом совместно с П. Бер-иайсом в “Основаниях математики”. Д. Гильберта интересовала непротиворечивость всей математики и, в частности, непротиворечивость доказательств основных теорем. Для того, чтобы проверить корректность доказательства за разумное время, необходимо, чтобы само доказательство было разумного размера. Отсюда возникает важный вопрос о сложности систем доказательств, изучение которого было инициировано работой [21]: в естественном предположении, что каждый шаг доказательства проверяется за полиномиальное время, требуется оценить количество шагов доказательства.
Пропозициональной системой доказательств называется система доказательств для языка TAUT пропозициональных тавтологий в ДНФ. Поскольку такой язык содержится в co-NP, то любую систему доказательств для co-NP-трудного языка L можно считать пропозициональной системой доказательств, для этого необходимо лишь зафиксировать конкретное сведение.
С практической точки зрения системы доказательств интересны тем, что обобщают понятие алгоритма. За одной фиксированной системой доказательств П скрывается целое семейство алгоритмов, оперирующих правилами П. Если мы доказали невозможность существования короткого доказательства для тавтологии я, значит все алгоритмы, применяющие правила из П, будут долго работать на я вне зависимости от того, в каком порядке применяются правила.
Одними из самых известных системам доказательств являются системы Фреге, к которым, например, относятся системы гильбертовского
-6-
типа и генцсиовская система с правилом сечения. С. А. Кук и Р. А. Рекхоу в [21] доказали, что различные системы Фреге полиномиально моделируются друг в друге. Для них, в частности, известны верхние полиномиальные оценки для семейств формул, кодирующих принцип Дирихле [10| и нераскрашиваемость графа, содержащего клику [54], имеющих экспоненциальную сложность, например, в резолюционной системе доказательств.
Для частного случая систем Фреге, систем Фреге ограниченной глубины, доказано несколько экспоненциальных нижних оценок [52,12,13,18, 45]. Эти системы отличаются от исходных константными ограничениями на глубину промежуточных формул.
Многие системы доказательств не имеют коротких выводов простых фактов, например, известная резолюциоиная система доказательств, введённая в [55], не имеет короткого доказательства принципа Дирихле. С другой стороны, можно естественным образом переписать данную формулу в виде системы линейных неравенств, например, записав каждую дизъюнкцию следующем образом:
V ъ V V -'Уі -> XХі+В1 - -*•
Далее, при помощи полуалгебраических систем доказательств можно выводить из неравенств новые полиномиальные неравенства, являющиеся полуалгебраическими следствиями искомых. В частности, для принципа Дирихле в используемых полуалгебраических системах это приводит к короткому доказательству. На эффективность данной техники для других тавтологий мог бы позволить надеяться предложенный в 1979 Л. Г. Хачия-ном полиномиальный алгоритм решения задачи линейного программирования, а также различные алгоритмы, основанные на методе внутренней точки.
-7-
Полуалгебраические системы доказательств
Первая полуалгебраическая система доказательств, “секущие плоскости” (СР), оперирующая только линейными неравенствами, была введена в 60-70 годах прошлого века в работах [26,19, 22]. Система основана на простом соображении о том, что сумма целых чисел также должна быть целым числом. Доказательство нижней экспоненциальной оценки для системы “секущие плоскости” долгое время оставалось важным открытым вопросом. В работе [25] была доказана нижняя экспоненциальная оценка для СР с ограниченной степенью ложности (т.е. с ограничением на свободный член неравенства), в работах [15, 41] для СР с унарными (полиномиально ограниченными) коэффициентами, в работах [36, 43] для древовидных “секущих плоскостей”, в которых мы не имеем возможности использовать уже доказанные факты многократно и обязаны выводить их каждый раз заново. Для системы без ограничений нижняя экспоненциальная оценка была доказана в [53] для формул, кодирующих ослабленный принцип нераскрашиваемости графа, содержащего клику. Нижняя экспоненциальная оценка для системы “поднять и спроецировать” (Ь&Р) [9], что также оперирует только линейными неравенствами, была доказана техникой, аналогичной технике доказательства вышеупомянутых нижних оценок для СР, в работе [24].
В разделе 3.2 данной диссертации приводится способ преобразования Ь&Р-доказательства в доказательство в СР размера, полиномиально зависящего от размера исходного доказательства и коэффициентов в нём, из которого следует, например, альтернативный метод доказательства нижней экспоненциальной оценки для системы Ь&р1 с унарными коэффициентами.
Для системы Ловаса-Схрайвера (ЬЭ) [48, 47], оперирующей квадратичными неравенствами, нижние экспоненциальные оценки были известны только для древовидных доказательств систем неравенств, не облада-
- Київ+380960830922