Geodesic
Refinement of bounds of the heights of terms in the most general unifer
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 117-134

Voir la notice de l'article provenant de la source Math-Net.Ru

We consider the most general unifer of a pair of terms. Our goal is to estimate the heights of terms in the unifer respect to the depth differences of variables in given terms. The depth difference of a variable is the maximum of the differences between the depths of occurrences of the variable in the terms. Such bounds are useful in finding upper bounds of the heights of terms in proofs in Gentzen-type sequential calculi. We construct a series of examples proving an exponential lower bound on the heights of terms in the most general unifer. We also improve the previously known upper bound of heights in the most general unifer. 
@article{ZNSL_1997_241_a4,
     author = {B. Yu. Konev},
     title = {Refinement of bounds of the heights of terms in the most general unifer},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {117--134},
     publisher = {mathdoc},
     volume = {241},
     year = {1997},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a4/}
}
TY  - JOUR
AU  - B. Yu. Konev
TI  - Refinement of bounds of the heights of terms in the most general unifer
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1997
SP  - 117
EP  - 134
VL  - 241
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a4/
LA  - ru
ID  - ZNSL_1997_241_a4
ER  - 
%0 Journal Article
%A B. Yu. Konev
%T Refinement of bounds of the heights of terms in the most general unifer
%J Zapiski Nauchnykh Seminarov POMI
%D 1997
%P 117-134
%V 241
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a4/
%G ru
%F ZNSL_1997_241_a4
B. Yu. Konev. Refinement of bounds of the heights of terms in the most general unifer. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 117-134. http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a4/