Разрешимые классы, сводящиеся к однокванторному классу

Рассматривается разрешимость по выводимости в классическом исчислении предикатов с функциональными знаками (без равенства); понятие $F$-префикса и тип рассматриваемых формул см. в РЖМат, 1967, 5А74. $F\in N_2$ тогда и только тогда, когда всякий терм из $F$ содержит не более одной переменной и всякий $F$-префикс, длина которого больше 1, кончается $\forall$-квантором. Доказана разрешимость класса произвольных дизъюнкций из $N_2$ (оба наложенных на $F$ из $N_2$ условия необходимы). В $N_2$ попадает (после сколемизации) ряд известных разрешимых классов, в частности класс $N_1$ формул, содержащих не более одного $\exists$-квантора. Рассмотрен разрешимый класс, полученный из $N_1$ так же, как $K'$ из $K$ (РЖМат, 1969, 2А100). Основной аппарат доказательства – обратный метод (с использованием минископизаций и моделирования благоприятных наборов).
Библ. 11 назв.