12.12.2017 Нижняя оценка на доказательство формулы в системе OBDD(and, reordering) (Марсель Матдинов)

Название: Нижняя оценка на доказательство формулы в системе OBDD(and, reordering)

Время: 12 декабря, 16:30

Место: ПОМИ РАН, ауд. 402

Докладчик: Марсель Матдинов

Описание:

Будет продолжено доказательство того, что любое доказательство формулы PHP(n, l*n) в системе OBDD(and, reordering), где l - некоторая константа, большая единицы, имеет экспоненциальный от n размер. Текст доказательства в приложении

В прошлый раз была сформулирована лемма 1 и доказаны утверждения 2 и 3, нужные для ее доказательства

Текст доказательства в  приложении.