Специализация формы вывода в исчислении предикатов с равенством и функциональными символами. I

В работе строится секвенциальный свободный от сечения вариант исчисления предикатов с равенством и функциональными символами. Доказывается ряд теорем о специализации формы вывода в этом исчислении, связанных с наложением ограничений на применения правил для равенства. Библ. 5 назв.