Упорядоченные диаграммы принятия решений (OBDD) - это частный случай однопроходных ветвящихся программ, в которых переменные встречаются в определенном порядке. Наложенное ограничение позволяет эффективно выполнять многие операции с булевыми функциями, записанными в этом виде. В 2004 году Атсериас, Варди и Колайтис предложили систему доказательств, в которых строки доказательств записываются в виде OBDD, из двух OBDD можно выводить любую OBDD, которая из них семантически следует. В 2008 году Крайчек доказал экспоненциальную нижнюю оценку в этой системе доказательств, если все OBDD в доказательстве используют одни и те же порядки на переменных. Если разрешить использовать в доказательствах OBDD в разных порядках, то получится строго более сильная система доказательств, для которой суперполиномиальных нижних оценок не известно.

В докладе мы рассмотрим исчисление однопроходных ветвящихся программ (1-BP), в котором можно выводить новые 1-BP как конъюнкцию уже имеющихся или как проекцию имеющейся 1-BP. Это семантическое обобщение некоторой подсистемы упомянутой выше OBDD-системы доказательств, в которой можно использовать различные порядки на переменных в OBDD. Мы покажем, что существует семейство невыполнимых формул $F_n$ в O(1)-КНФ и константа C, что любой вывод в этом исчислении, использующий проекции по не более, чем Cn различным переменным, имеет размер хотя бы $2^{\Omega(n)}$.

Доклад основан на совместной работе с С. Басом, А. Кнопом, А. Рязановым и Д. Соколовым.