О построении консервативных логических выводов

Вывод называется консервативным, если в него входят только логические связки, входящие в нижнюю секвенцию. Исчисление И называется консервативным, если для каждой секвенции, выводимой в И, имеется консервативный вывод в И. Строятся консервативные односукцедентные секвенциальные варианты классического исчисления предикатов, приспособленные для поиска вывода. Строится также консервативный вариант натурального типа для классического исчисления предикатов. Библ. 10 назв.