Эрбрановы тактики и отношение “большей выводимости”

Эрбранова тактика $T$ – это алгорифм, который по произвольной предваренной формуле $F$ выдает последовательность ее эрбрановых разверток. Пусть $F^T$ – первая тавтология в этой последовательности. $T$ полна, если для любой выводимой $F$ существует $F^T$. Тактика $T$ дает для $F$ $k$ лишних членов, если из $F^T$ можно с сохранением тавтологичности выбросить $k$ дизъюнктивных членов; $T$ оптимальна для $F$, если для $F$ не существует эрбрановой дизъюнкции, короче $F^T$. Существует полная тактика, дающая для всех $F$ сколь угодно малую долю лишних членов. Более интересны тактики, работающие по неполной информации об $F$ (например, по сигнатуре $F$ или списку ее элементарных подформул). По любой такой полной тактике можно построить класс формул, для которых доля лишних членов стремится к $I$ (при увеличении длины формулы). Кроме того, даже для тактики, требующей полного и равномерного Перебора всех возможных (при данной сигнатуре) подстановок термов, невозможен алгорифм, выделяющий случаи, в которых не следует пользоваться этой тактикой: класс формул, для которых она оптимальна, неразрешим.
Для доказательств используются свойства отношения "$F$ более выводима, чем $G$", которое изучено в терминах общей теории исчислений. Библ. 13 назв.