Geodesic
Upper bound on the height of terms in proofs with bound-depth-restricted cuts
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VI, Tome 277 (2001), pp. 80-103 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

We prove an upper bound on the height of terms occurring in a most general unifier for the case when the set of term-variables splits to two subsets. A term-variable belongs to the first sub-set iff the depths of all its occurrences coincide, we call such a variable a term-variable of the cut type; otherwise, it belongs to the second sub-set. We bound from above the height of terms occurring in a most general unifier by the number of term-variables of not the cut type and size of the given unification problem. This bound implies an upper bound on the size of terms occurring in proofs in a sequent-style calculus with bound-depth-restricted cuts. 
@article{ZNSL_2001_277_a4,
     author = {B. Yu. Konev},
     title = {Upper bound on the height of terms in proofs with bound-depth-restricted cuts},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {80--103},
     year = {2001},
     volume = {277},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2001_277_a4/}
}
TY  - JOUR
AU  - B. Yu. Konev
TI  - Upper bound on the height of terms in proofs with bound-depth-restricted cuts
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2001
SP  - 80
EP  - 103
VL  - 277
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2001_277_a4/
LA  - ru
ID  - ZNSL_2001_277_a4
ER  - 
%0 Journal Article
%A B. Yu. Konev
%T Upper bound on the height of terms in proofs with bound-depth-restricted cuts
%J Zapiski Nauchnykh Seminarov POMI
%D 2001
%P 80-103
%V 277
%U http://geodesic.mathdoc.fr/item/ZNSL_2001_277_a4/
%G ru
%F ZNSL_2001_277_a4
B. Yu. Konev. Upper bound on the height of terms in proofs with bound-depth-restricted cuts. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VI, Tome 277 (2001), pp. 80-103. http://geodesic.mathdoc.fr/item/ZNSL_2001_277_a4/