Обычно под доказательством понимают некоторый текст, убеждающий читателя в справедливости некоторого утверждения. В математике подразумевается, что доказательство проверяется алгоритмически и может иметь вид цепочки формул некоторой логической системы, либо быть более общим. Например, предъявление решения головоломки доказывает, что решение существует. Если алгоритм проверки доказательства работает за полиномиальное время, то задача определения истинности относится к классу NP. Если рассмотреть вероятностные алгоритмы проверки, получится чуть более широкий класс MA. Это самый широкий класс, для которого есть "публикуемые доказательства", которые можно эффективно проверить без участия автора.
В теории интерактивных доказательств концепция полностью меняется. Теперь доказательство это не текст, а диалог, как на устном экзамене или докладе на научном семинаре. Участники диалога - прувер, стремящийся доказать некоторое утверждение, и верификатор, который должен проверить корректность. Прувер должен суметь доказать любое верное утверждение и не должен доказать никакое неверное (с высокой вероятностью). При этом прувер никак вычислительно не ограничен, а верификатор должен использовать только полиномиальные вероятностные вычисления. Класс доказуемых в этом смысле утверждений называется IP, мини-курс будет посвящён изучению этого класса и его вариаций. На первых двух лекциях мы изучим базовую теорию и докажем теорему IP=PSPACE. На следующих двух лекциях мы познакомимся с теорией доказательств с несколькими пруверами и новым подходом - теорией рациональных интерактивных доказательств.
Date and time | Class|Name | Venue|short | Materials |
---|---|---|---|
23 March 17:15–18:45 |
Базовая теория интерактивных доказательств, Lecture | ПОМИ РАН | video |
23 March 19:00–20:30 |
IP=PSPACE, Lecture | ПОМИ РАН | video |
24 March 11:15–12:45 |
Доказательства с несколькими пруверами, Lecture | ПОМИ РАН | video |
24 March 13:00–14:30 |
Рациональные интерактивные доказательства, Lecture | ПОМИ РАН | video |