Обратный метод и тактики установления выводимости для исчисления с функциональными знаками

Подробно излагается конкретизация обратного метода (РЖМат, 1969, 2А100), позволяющая устанавливать выводимость в классическом исчислении предикатов (для исходных формул произвольной структуры). Доказаны теоремы полноты ряда тактик (в различных сочетаниях), что позволяет жестко регламентировать переборы в процессе установления выводимости; особое внимание уделено тактикам, основанным на унификации порядка членов в благоприятных наборах. Установлена связь между сложностями обоснования благоприятности и генценовского вывода (за сложность последнего принимается число применений $\exists$-правил).
Библ. 24 назв.