Изменения

|definition=<tex>TQBF</tex> расшифровывается как '''True Quantified Boolean Formula. Это '''. Это язык верных булевых формул с кванторами'''.<br/><tex>TQBF=\{Q_1 x_1 Q_2 x_2 \cdots ldots Q_n x_n \phi(x_1, x_2, \dots, x_n), Q_i \in \{\forall, \exists\}\}</tex>.

Чтобы доказать, что <tex>TQBF \in \mathrm{PSC}</tex>, необходимо показать, что <tex>TQBF \in \mathrm{PSPSH}</tex> и <tex>TQBF \in \mathrm{PSHPS}</tex>.

<tex>solve(Q_1 x_1 Q_2 x_2 \cdots ldots Q_n x_n \phi(x_1, x_2, \dotsldots, x_n))</tex>

'''return''' <tex>solve(Q_2 x_2 \cdots ldots Q_n x_n \phi(0, x_2, \dotsldots, x_n)) \land solve(Q_2 x_2 \cdots ldots Q_n x_n \phi(1, x_2, \dotsldots, x_n))</tex>

'''return''' <tex>solve(Q_2 x_2 \cdots ldots Q_n x_n \phi(0, x_2, \dotsldots, x_n)) \lor solve(Q_2 x_2 \cdots dots Q_n x_n \phi(1, x_2, \dotsldots, x_n))</tex>

Так как <tex>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Пусть <tex>\Omega = |\Sigma \cup Q|</tex>.

Пусть <tex>I</tex> — конфигурация <tex>M</tex>. Размер конфигурации есть равен <tex>p(\Omega n)</tex>, где <tex>n</tex> — длина входа. Тогда всего конфигураций <tex>2^{\Omega n}</tex>. Введём обозначение <tex>x_{I, i,c}</tex> — в конфигурации <tex>I</tex> на <tex>i</tex>p-том месте стоит символ <tex>c</tex> — некоторый полином. Тогда выражение <tex>\exists I</tex> обозначает <tex> \exists x_0^x_{I ,1,c_1} \, \exists x_1^x_{I ,1,c_2} \dots ldots \exists x_{r(n)I,1,c_\Omega}^I</tex> \, где <tex>\exists x_{x_i^I,2,c_1} \}ldots</tex> — все переменные конфигурации <tex>I</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> \forall x_0^x_{I ,1,c_1} \, \forall x_1^x_{I ,1,c_2} \dots ldots \forall x_{r(n)I,1,c_\Omega}^ \, \forall x_{I</tex>. Всего конфигураций у ДМТ <tex>M \, 2^{O(p(n)),c_1}\ldots</tex>.

<tex>f(M, w) = (\exists I_{st}S \, \exists F \, (S - start) \land (F - accept) \land \exists I_phi(S, F, log_2(2^{fin\Omega n}) (x_0^))</tex>. Выражения <tex>S - start</tex> и <tex>F - accept</tex> можно записать следующим образом: <tex>S - start = x_{I_{stS, 1, w[1]}} = start \land x_1^x_{I_{st}} = S, 2, w[12] } \land \dots ldots \land x_{S, |w|}^{I_{st}} = , w[|w|]) } \land (x_{S, |w| + 1, B} \ldots \exists i land x_{S, \Omega , x_i^B}</tex>. <tex>F - accept = x_{I_{finS, |w| + 1, \#_y}} = finish) \land lor \ldots \phi(I_lor x_{st}S, I_{fin}\Omega, log_2(2^{O(p(n))\#_y})))</tex>. 

Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{O(p(\Omega n))}</tex>, а значит формула <tex>\phi</tex> верна.

Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{O(p(\Omega n))}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</tex>.