Оглавление
Введение
Основные определения и обозначения.
Актуальность темы и исторический обзор.
Системы доказательств для пропозициональной логики
Алгоритмы для задач пропозициональной логики
Результаты настоящей диссертации, их публикация и дальнейшее
развитие .
Системы доказательств для пропозициональной логики
Алгоритмы для задач пропозициональной логики
Структура диссертации
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 и ЬЭ4 .
1.3.3 Рассуждения о целых числах в нолуалгебраических системах .
1.3.4 Короткие доказательства цейтииских тавтологий в системе
1.3.5 Линейная нижняя оценка на булеву степень
опровержения симметричной задачи о рюкзаке в РозНувеепзагисчислеиии
1.3.6 Экспоненциальная нижняя оценка на размер выво
да в статическом варианте Ь8 и в РозШувеепваяисчислении.
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 Детерминированный алгоритм для задачи МАХ28АТ, основанный на методе расщепления
Литература
- Київ+380960830922