Notice that decidability of admissible rules of a decidable logic is equivalent to the existence of recursive (or recursively enumerable) bases: on the one hand, the set of "all" admissible rule is a recursive basis if admissibility is decidable. On the other hand, the set of admissible rules is always co-r.e., and if we further have an r.e. basis, it is also r.e., hence it is decidable. (In other words, we can decide admissibility of "A"/"B" by the following algorithm: we start in parallel two exhaustive searches, one for a substitution σ which unifies "A" but not "B", and one for a derivation of "A"/"B" from "R" and formula_7. One of the searches has to eventually come up with an answer.) Apart from decidability, explicit bases of admissible rules are useful for some applications, e.g. in proof complexity.