Секвенциальные варианты прикладных исчислений предикатов без структурных правил вывода

Устанавливается результат о специализации формы вывода в исчислении предикатов с равенством (возможность ограничиться “сукцедентными применениями” правил для равенства), допускающий многочисленные приложения. В качестве приложения этой леммы доказывается теорема о нормализации для исчисления предикатов с равенством. Строятся свободные от сечения и не содержащие других структурных правил генценовские варианты для аксиоматически охарактеризованных математических теорий, задаваемых конечным списком или перечислимым множеством специфических аксиом и имеющих в качестве аппарата логического вывода логические средства классического исчисления предикатов первой ступени с постоянными функциональными знаками и равенетвом (любая такая математическая теория называется прикладным исчислением предикатов).
Библ. 22 назв.