Unification
One of the main ingredients in the inference mechanism is the process of making atomic formulas syntactically equivalent. This process, called unification, is a procedure that take two atomic formulas as input, and either shows how they can be instantiated to identical atoms or, reports a failure.
Definition (Renaming)
A substitution ${X_1/Y_1, …X_n/Y_n}$ is called a renaming substitution iff $Y_1, …, Y_n$ is a permutation of $X_1, …, X_n$.
A renaming substitution represents a bijective mapping between variables (or more generally terms). Such a substitution always preserves the structure of a term; if $\theta$ is a renaming ant $t$ is a term, then $t\theta$ and $t$ are equivalent but for the names of the variables. Now, the fact that a renaming represents a bijection implies that there must be an inverse mapping. Indeed, if ${X_1/Y_1, X_n/Y_n}$ is a renaming then ${Y_1/X_1, …, Y_n/X_n}$ is its inverse. We denote the inverse of $\theta$ by $\theta^{-1}$ and observe that $\theta\theta^{-1}=\theta^{-1}\theta=\epsilon$.