|
Труды ордена Ленина Математического института имени В. А. Стеклова, 1972, том 121, страницы 57–66
(Mi tm3111)
|
|
|
|
Разрешимые классы, сводящиеся к однокванторному классу
С. Ю. Маслов, В. П. Оревков
Аннотация:
Рассматривается разрешимость по выводимости в классическом исчислении предикатов
с функциональными знаками (без равенства); понятие $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 назв.
Образец цитирования:
С. Ю. Маслов, В. П. Оревков, “Разрешимые классы, сводящиеся к однокванторному классу”, Логические и логико-математические исчисления. 2, Тр. МИАН СССР, 121, 1972, 57–66; Proc. Steklov Inst. Math., 121 (1972), 61–72
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tm3111 https://www.mathnet.ru/rus/tm/v121/p57
|
Статистика просмотров: |
Страница аннотации: | 144 | PDF полного текста: | 73 |
|