Новый разрешимый хорновский фрагмент исчисления предикатов

В работе описано расширение хорновского варианта класса формул $\forall\exists$. Для секвенций из этого класса доказана разрешимость проблемы выводимости в исчислении предикатов. Найдены сложностные характеристики, фиксация которых разбивает это расширение на полиномиально разрешимые подклассы. Фиксация максимальной размерности предикатов разбивает рассматриваемое расширение на подклассы, принадлежащие NP. Библ. – 11 назв.