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

Предлагается алгоритм, обладающий двумя свойствами: он не использует сведения к разрешимости другой теории (как алгоритм Рабина) и имеет оптимальную верхнюю оценку времени – в отличие от алгоритма Лёйхли и Леонарда, для которого вообще нет явной верхней оценки времени.
Библиогр. 3 назв.