Сложность пропозициональной логики

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

Оглавление
Введение
Основные определения и обозначения
Актуальность темы и исторический обзор
Системы доказательств для пропозициональной логики
Алгоритмы для задач пропозициональной логики
Результаты настоящей диссертации, их публикация и дальнейшее
развитие
Системы доказательств для пропозициональной логики
Алгоритмы для задач пропозициональной логики
Структура диссертации
1 Системы доказательств для пропозициональной логики
1.1 Определения, связанные с системами доказательств
1.1.1 Понятие системы доказательств
1.1.2 Традиционные системы доказательств
1.1.3 Алгебраические системы доказательств
1.1.4 Полуалгебраические системы доказательств
1.1.5 Секвенциальные системы, основанные на неравенствах .
1.1.6 Системы, использующие строгие неравенства
1.1.7 Формульные алгебраические системы
1.2 Формульные алгебраические системы

1.2.1 Моделирование систем Фреге в системе Р-РС
1.2.2 Полиномиальная эквивалентность системы Р-ИЯ и древесного вывода в системе Р-РС
1.2.3 Короткие доказательства пропозиционального принципа Дирихле в системах ограниченной глубины
1.3 Полуалгебраические системы
1.3.1 Способы перевода пропозициональных формул для ис-
пользования в и верхние оценки на степень доказательств
1.3.2 Короткие доказательства тавтологий, кодирующих
нераскрашиваемость графа, содержащего клику, в системах ЬБ + СР2 и ЬЭ
1.3.3 Рассуждения о целых числах в полуалгебраических системах
1.3.4 Короткие доказательства цейтинских тавтологий в системе
1.3.5 Линейная нижняя оценка на “булеву степень”
опровержения симметричной задачи о рюкзаке в РозШу81е11еп8а1г-исчислении
1.3.6 Экспоненциальная нижняя оценка на размер выво-
да в статическом варианте Ь3+ и в Ро81Ну81е11еп8а1г-исчислении
1.3.7 Секвенциальные системы, основанные на линейных
неравенствах
1.3.8 Система секущих плоскостей с ограниченной степенью
ложности

2 Алгоритмы для пропозициональной логики
2.1 Алгоритмы для задачи выполнимости пропозициональных
формул
2.1.1 Обозначения и соглашения
2.1.2 Детерминированные алгоритмы, основанные на методе локального поиска
2.1.3 Экспериментальный вероятностный алгоритм, основанный на комбинации методов локального поиска и кодирования выполняющего набора
2.2 Алгоритмы для задачи максимальной выполнимости
2.2.1 Определения, связанные с задачей максимальной выполнимости
2.2.2 Вероятностный алгоритм для задачи МАХ-/с-БАТ, основанный на методе локального поиска
2.2.3 Детерминированный алгоритм для задачи МАХ-2-ЭАТ, основанный на методе расщепления
Литература

применять и к квадратичным неравенствам: а^хіхі + ^^ щзд с
---------=---------------— (где йі,йіп Є £, Хі — переменная). (1.15)
'lІjXiXj "р / &іХі ^ І С [
1.1.4.3 Системы большей степени
Определим теперь полуалгебраические системы, использующие полиномы большей степени (вплоть до некоторой степени бГ).
ЬБ^. Эта система расширяет систему ЬБ, а именно, правило (1-11) разрешается применять к / степени вплоть до б? — 1, а не только к линейным
неравенствам. Правило (1.8) разрешается применять к любому набору
неравенств степени вплоть до степени й.
Замечание 1.2. Мы используем те же обозначения и для сі = оо, т.е. в случае, когда степень не ограничена.
Замечание 1.3. Заметим, что ЬБ = ЬБ2.
Аналогичным образом мы будем рассматривать системы ЬБ+, и
ЬБ+*, изменяя условия линейности полиномов I (/,д соответственно) в (1.13) (и (1.14), соответственно), на условия “ск^(£2) ^ сГ (соответственно, !Меё(./.9) < <г).
1.1.4.4 Статические системы
Статическими мы будем называть системы, доказательство в которых состоит из полиномов, удовлятворяютдих некоторому ограничению, а не представляет собой последовательный вывод одних равенств или неравенств из других. Статические системы обычно имеют нестатические аналоги, которые являются их естественным обобщением. Например, система Миіізіеііепваїг является “статической” версией полиномиального исчисления;