filmov
tv
[Коллоквиум]: Теория сложности доказательств
Показать описание
Докладчик: Александр Разборов - Университет Чикаго/МИАН
Теория сложности доказательств изучает насколько простыми могут (или не могут) быть формальные доказательства истинных утверждений в различных естественных системах доказательств. Классы рассматриваемых утверждений и систем могут существенно варьироваться в зависимости от контекста, что определяет целый ряд неожиданных и важных взаимосвязей между теорией сложности доказательств и многими областями в математике и компьютерных науках. Весьма значительную часть всей теории занимают пропозициональные доказательства, т.е. доказательства бескванторных утверждений, представимых в языке логики высказываний.
В своём обзорном докладе Александр дает краткое введение в эту последнюю область. Две темы, которым уделено особое внимание ввиду их актуальности, таковы:
1. Система резолюций и практические алгоритмы для выполнимости булевых формул.
2. Алгебраические и полуалгебраические системы доказательств и комбинаторная оптимизация.
Теория сложности доказательств изучает насколько простыми могут (или не могут) быть формальные доказательства истинных утверждений в различных естественных системах доказательств. Классы рассматриваемых утверждений и систем могут существенно варьироваться в зависимости от контекста, что определяет целый ряд неожиданных и важных взаимосвязей между теорией сложности доказательств и многими областями в математике и компьютерных науках. Весьма значительную часть всей теории занимают пропозициональные доказательства, т.е. доказательства бескванторных утверждений, представимых в языке логики высказываний.
В своём обзорном докладе Александр дает краткое введение в эту последнюю область. Две темы, которым уделено особое внимание ввиду их актуальности, таковы:
1. Система резолюций и практические алгоритмы для выполнимости булевых формул.
2. Алгебраические и полуалгебраические системы доказательств и комбинаторная оптимизация.