Сложность пропозициональных систем доказательств, оперирующих неравенствами

• Автор: Кожевников, Арист Александрович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2007
• Место защиты: Санкт-Петербург
• Количество страниц: 96 с.

Полуалгебраические системы доказательств

Статические полуалгебраические системы доказательств

Полуалгебраические системы доказательств генценовского типа

Полуалгебраические системы с ограниченной степенью ложности 10 Структура диссертации

1 Используемые системы доказательств и семейства тавтологий

1.1 Пропозициональные системы доказательств

1.2 Алгебраические системы доказательств

1.3 Полуалгебраические системы доказательств

1.4 Статические полуалгебраические системы доказательств

1.5 Полуалгебраические системы доказательств генценовского

типа
1.6 Понятие степени ложности
1.7 Понятия и обозначения теории графов
1.8 Формулы, кодирующие принцип Дирихле
1.9 Формулы, кодирующие принцип нераскрашиваемости графа, содержащего клику
1.10 Цейтинские формулы на графах-расширителях
2 Сложность статических полуалгебраических систем
2.1 Короткое статическое доказательство тавтологии о нераскрашиваемости графа, содержащего клику

2.2 Нижние экспоненциальные оценки на длину вывода цейт-инских формул в статической полуалгебраической системе доказательств Ловаса-Схрайвера
2.2.1 Процедура очищения расширителей
2.2.2 Линейная нижняя оценка на булеву степень вывода биномиальных цейтинских формул в системе доказательств РБ
2.2.3 Нижние оценки па булеву степень РЭ-доказательства биномиальных цейтинских формул
2.2.4 Преобразование доказательства цейтинских формул в статической Ь3+ в доказательство в РЭ
2.2.5 Нижняя экспоненциальная оценка на размер доказательства в статической Ь3+
3 Сложность полуалгебраических систем генценовского типа
3.1 Полиномиальная эквивалентность ЩЬ&Р) и Л(ЬР), связь ЩСР) и ЩЬР)
3.2 Полиномиальное моделирование Ь&Р1 в СР1
3.3 Доказательство полиномиального размера цейтинских формул в 11(ЬР)
3.4 Вещественная коммуникационная сложность и нижние экспоненциальные оценки для Л(СР)
4 Сложность полуалгебраических систем с ограниченной степенью ложности
4.1 Верхние полиномиальные оценки на размер доказательств принципа Дирихле и принципа нераскрашиваемости графа, содержащего клику
4.2 Полиномиальное моделирование ЬЗ^'+СР^ с ограниченной степенью ложности в 11ез(/с)
Нижние экспоненциальные оценки для ЬЭА+СРА с линейной от количества переменных степенью ложности

Для полуалгебраической статической системы ЬБ+ пропозициональная формула, записывающая цейтинские формулы (1.26) для графа С?, (г, ф с)-расширителя, будет записываться следующем множеством неравенств:
/£,;=£ *« + £(1-*е)-1> 0 (2.18) ее5„5;
для каждой вершины V € V' и каждого подмножества Б1' чётной мощности множества смежных с вершиной г» рёбер и для каждой вершины д £ V V' и каждого подмножества Б[, нечётной мощности множества Яь, смежных с вершиной V рёбер.
Эквивалентная запись пропозициональной формулы (1.26) для алгебраической статической системы доказательств ЬЭ+ в виде множества равенств будет иметь следующий вид:
Л";= П (1-Щ'Пхе = о (2.19)
ее5„5' еб5;
для каждой вершины V и каждого подмножества Й”' чётной мощности множества смежных с вершиной у рёбер и для каждой вершины V € V V' и каждого подмножества 5' нечётной мощности множества Яу смежных с вершиной V рёбер.
Лемма 2.13 Пусть дано доказательство Р булевой степени к системы равенств (2.19), расширенной равенствами х — хе = 0,е € Е в РБ, тогда существует доказательство Р' системы равенств (1.27), расширенной равенствами у2е — 1 = 0, е е Е, в системе доказательств РБ булевой степени, не превосходящей к + (I.
Доказательство. Запишем доказательство Р следующим образом:
Л • ЗД + - ®е) • & = 1 + Ь*
для всех соответствующих подмножеств рёбер смежных с вершиной и. Выразим пропозициональные переменные хг-, г £ /, через переменные уг-,