|
Труды ордена Ленина Математического института имени В. А. Стеклова, 1972, том 121, страницы 5–13
(Mi tm3109)
|
|
|
|
Об ограничении сложности термов в методе резолюций
Н. К. Замов
Аннотация:
Терм $f^{(n)}t_1\dots t_n$ называется регулярным, если любой его подтерм положительного
ранга имеет вид $g^{(m)}t_1\dots t_m$, где $m<n$. Доказывается ряд лемм о регулярных термах. В частности,
показано, что ранг регулярного терма $f^{(n)}t_1\dots t_n$ не больше, чем $n-m+1$, где $n$ –размерность функционального символа $f^{(n)}$, $m$ – минимальная из размерностей функциональных
символов, входящих в $t_1\dots t_n$. В работе указаны некоторые классы формул, для
которых при установлении доказуемости методом резолюций достаточно строить выводы,
содержащие лишь дизъюнкты с регулярными термами. В частности, для класса почти сколемовских формул можно строить лишь такие выводы, что ранги термов в дизъюнктах не превышают 1.
Библ. 5 назв.
Образец цитирования:
Н. К. Замов, “Об ограничении сложности термов в методе резолюций”, Логические и логико-математические исчисления. 2, Тр. МИАН СССР, 121, 1972, 5–13; Proc. Steklov Inst. Math., 121 (1972), 1–10
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tm3109 https://www.mathnet.ru/rus/tm/v121/p5
|
Статистика просмотров: |
Страница аннотации: | 159 | PDF полного текста: | 80 |
|