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
Citer cet article
Voir la notice du chapitre de livre provenant de la source Math-Net.Ru
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.