СПб.: Санкт-Петербургский государственный университет;
Санкт-Петербургское отделение Математического института им.
В.А.Стеклова (ПОМИ) РАН, Гирш Э.А., 2010 г.
Курс лекций, прочитанный в Санкт-Петербургском государственном
университете, посвящён оценкам длины доказательств в первую очередь
для утверждений логики высказываний, хотя будут рассмотрены и
другие языки. Существование системы, в которой есть доказательство
полиномиальной длины для каждой тавтологии, эквивалентно
(неправдоподобному) утверждению NP = co-NP. Однако на констатации
этого факта вопросы не заканчиваются: даже если такой системы нет,
есть ли "оптимальная" система с самыми короткими доказательствами?
Для каких систем мы можем доказать экспоненциальные нижние оценки
на длину доказательств? Как длины доказательств связаны со
сложностью вычислительных задач? Подобным вопросам и посвящён этот
курс.
Материал включает в себя конспекты лекции, презентации и вопросы к
экзамену.
Введение.
Системы Фреге.
Моделирование секущих плоскостей в системах Фреге, оптимальные системы.
Непересекающиеся NP-пары.
Нижняя оценки для CP. Нижняя оценка для цейтинских формул в Res.
Нижние оценки для принципа Дирихле и корректности метода резолюций.
Связь сложности древесных доказательств и коммуникационной сложности.
Системы Фреге.
Моделирование секущих плоскостей в системах Фреге, оптимальные системы.
Непересекающиеся NP-пары.
Нижняя оценки для CP. Нижняя оценка для цейтинских формул в Res.
Нижние оценки для принципа Дирихле и корректности метода резолюций.
Связь сложности древесных доказательств и коммуникационной сложности.