Верхняя оценка высоты термов в выводах с сечениями по формулам ограниченной глубины связанных вхождений

Доказана верхняя оценка высоты термов, входящих в наиболее общий унификатор, для случая, когда множество неизвестных разбивается на два класса. Неизвестная принадлежит к первому классу, если глубины всех ее вхождений совпадают; мы называем такую неизвестную неизвестной типа сечения. Неизвестные второго типа (неизвестные не типа сечения) могут иметь вхождения произвольной глубины. Мы оцениваем сверху высоту термов в наиболее общем унификаторе в терминах количества неизвестных не типа сечения и высоты задачи унификации. Из данной оценки вытекает верхняя оценка размера термов, входящих в доказательства в секвенциальном исчислении с сечениями, при условии, что глубина связанных вхождений переменных в формулы сечения ограничена. Библ. – 18 назв.