Сложность разрешения теории первого порядка алгебраически замкнутых полей

Описан алгоритм, строящий по всякой формуле теории первого порядка алгебраически замкнутых полей эквивалентную ей бескванторную за время, полиномиальное от $\mathscr L^{n^{2a+1}}$, где $\mathscr L$ – размер формулы, $n$ – число переменных, $a$ – число перемен кванторов.
Библиография: 15 названий.