edit: Interestingly, the authors also state at one point that the choice of introduction rule is determined by the structure of the previous goal and the list of introduction rules; but at another point, that the choice of introduction rule is determined by the structure of the current goal and the list of introduction rules. I believe the latter is correct, but I'll have to be more careful implementing the paper's algorithm than I previously thought.
In any case, I believe the "no variable can relatively bind itself" restriction intends to preclude abstraction on a variable using that variable, but I could be wrong. If anything rests on whether or not this is correct, I'll attempt to contact the authors.
original: In a paper on natural deduction proof search, the authors write that the free variables $\gamma_1,\ldots,\gamma_n$ occurring in the formulae $\forall \alpha.\phi(\alpha,\gamma_1,\ldots,\gamma_n)$ and $\exists \alpha . \phi(\alpha,\gamma_1,\ldots,\gamma_n)$ in the conclusions of the quantifier introduction rules $\frac{\phi(\alpha/\beta,\gamma_1,\ldots,\gamma_n)}{\forall \alpha . \phi(\alpha,\gamma_1,\ldots,\gamma_n)} \quad (\forall\text{-in})$ and $\frac{\phi(\alpha/t)}{\exists \alpha . \phi (\alpha,\gamma_1,\ldots,\gamma_n)}\quad(\exists\text{-in})$ are relatively flagged or bound. Presumably, then, a variable is relatively bound if and only if it occurs free in the conclusion of a quantifier introduction rule. However, in defining a natural deduction derivation and presenting algorithms, they remark that no variable may relatively bind itself. For instance, they require that unification not produce substitutions causing variables to relatively bind themselves.
I searched through several logic books I had lying around, especially ones focusing on automated reasoning, but couldn't find a definition of relatively bound variables. Has anyone encountered this term before? If so, what does it mean?