ABSTRACT
The elim ination algorithm s discussed so far proceeded by recursion on the length of a derivation D and proceeded downwards in the tree of D , starting from the k -cu ts in maximal position. There are situations more general than the ones considered presently (which w ill occur in Book 3 ) in which one studies a more general sort of derivations, and for them it is not possib le to assign a finite number as their length. MINTS 75 has invented an elim i nation algorithm which uses recursion on the height of nodes and proceeds by ascending the tree of D upwards. The machinery of th is algorithm, how ever, can already be explained here, and it may even become clearer if no additional concepts distract the reader's attention.
