Об ограничении сложности термов в методе резолюций

Терм $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 назв.