О сложности логического вывода в генценовских системах

[alex_dorin]

Примем за сложность вывода секвенции количество применений правил в генценовсклй системе, необходимое для закрытия секвенции.
Вопрос : происходит ли уменьшение сложности вывода в процессе поиска доказательства обратным методом в генценоских системах без структурных правил вывода для логики первого порядка ?

C Уважением
А. Дорин