This preprint was accepted August 30, 1998
Contact:
B. Konev
ABSTRACT:
We describe an upper bound on the heights of terms occurring in a most general
unifier of a system of pairs of terms that contains unknowns of two types. An
unknown belongs to the first type if all occurrences of this unknown have the
same depth; we call such unknown an unknown of the cut type. Unknowns of the
second type (unknowns of not the cut type) are unknowns that have arbitrary
occurrences. We bound from above the heights of terms occurring in a most
general unifier in terms of the number of unknowns of not the cut type and of
the height of the system. This bound yields an upper bound on the sizes of
proofs in the Gentzen sequent calculus LK. Namely, we show that one can
transform a proof D in LK by substituting some free terms in places of
variables in such a way that the heights of terms occurring in the proof may
be bounded from above by $ar[D]^{h_1} \cdot q^{-}[D] \cdot h_0$, where ar[D]
is the maximal arity of function symbols occurring in D, $h_1$ is the maximal
height of terms occurring in analysis of the cut rules, $h_0$ is the maximal
height of terms occurring in $S$ and in side formulas of applications of the
cut rule, and $q^{-}$ is the number of analysis of applications of the
rules $\;\to\exists\;$, $\;\forall\to\;$ in D.