68
правок
Изменения
Нет описания правки
|statement=<tex> \forall L \in PS \Rightarrow L \leq_p TQBF</tex>
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>. Построим функцию <tex>f : \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>
Так как <tex>L \in PSPACE</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное время на ленте полиномиального размера.
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> ( \exists x_1 )\land( \exists x_2 )\land\dots\land( \exists x_n ) </tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Теперь рассмотрим два мгновенных описание <tex>M : A</tex> и <tex>B</tex>. Напишем полиномиальную рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в TQBF.
<tex>\phi(A, B, t) = (\exists R) (\forall U) (\forall V) (\neg(\phi(U, V, t/2)) \rightarrow ((U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S))</tex>
}}
