Уточнение оценок высоты термов в наиболее общем унификаторе

Рассматривается наиболее общий унификатор пары термов. Нас интересуют оценки высоты термов в наиболее общем унификаторе в терминах разностей глубин входящих в данные термы переменных. Под разностью глубин переменной понимается максимум разностей глубин вхождений переменных в данные термы. Подобные оценки могут применяться для оценки высот термов в доказательствах в секвенциальных исчислениях генценовского типа.
Строится семейство примеров, доказывающих экспоненциальный характер нижней оценки высот термов в наиболее общем унификаторе. Уточняются ранее известные верхние оценки высот термов в наиболее общем унификаторе. Библ. – 7 назв.