68
правок
Изменения
Нет описания правки
|statement=<tex>\mathrm{TQBF} \in \mathrm{PS}</tex>.
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
<tex>solve(k, Q_k x_k \ldots Q_n x_n \phi(x_k, \ldots, x_n))</tex> '''if''' <tex>k == n</tex> '''if''' <tex> nQ_k = \forall</tex> '''return''' <tex>\phi(0) \land \phi(1)</tex> '''if''' <tex>Q_k = \exists</tex> '''return''' <tex>\phi(0) \lor \phi(1)</tex>
'''if''' <tex>Q_k = \forall</tex>
'''return''' <tex>solve(Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(0, x_{k+1}, \ldots, x_n)) \land solve(Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(1, x_{k+1}, \ldots, x_n))</tex>
