68
правок
Изменения
Нет описания правки
|about=1
|statement=<tex>TQBF \in PSPASE</tex>
|proof=Чтобы доказать это, просто приведём программу<tex>solve</tex>, которая требует решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работает работающую за конечное время.
<tex>solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))</tex>
'''if''' <tex>Q_1 == \forall</tex>
'''if''' <tex>Q_1 == \exists</tex>
'''return''' <tex>solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \lor solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))</tex>
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
}}
{{Лемма
