Правило сечения в методе резолюций

В работе метод резолюций расширяется новым правилом, которое аналогично правилу сечения генценовских секвенциальных исчислений. Получены верхние и нижние оценки сложности опровержений с аналогом правила сечения и без этого правила. Сложность опровержений сравнивается также со сложностью секвенциальных доказательств с сечениями по формулам, которые не содержат импликаций, конъюнкций и квантора $\exists$ и в которые отрицание может входить только непосредственно перед элементарными формулами. Библ. – 3 назв.