Рассматриваются классы A, B замкнутых формул узкого исчисления предикатов (без равенства). Класс A состоит из всех формул, которые содержат лишь одноместные предикатные символы и имеют в предваренной нормальной форме кванторный префикс ∀∃∃; формулы класса B имеют кванторный префикс вида ∀x∃y₁∃y₂∀z, содержат лишь двуместные предикатные символы и не содержат атомарных формул вида P(z,x), P(z,y₁), P(z,y₂). Через Sat(A) (соотв. Sat(B)) обозначается множество всех выполнимых формул класса A (класса B), а через DT(T(n)) - класс множеств, распознаваемых одноленточными детерминированными машинами Тьюринга за время T(n). Доказано, что для подходящих констант a>b>1 выполняются соотношения
Sat(A) ∈ DT(a^n/logn)\DT(b^n/logn), Sat(A) ∈ DT(a^an/logn)\DT(b^bn/logn).

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

Математические вопросы и теория численных методов