In this paper the problems of solvability and right-invertibility for implicit nonlinear discrete-time control systems are investigated. The concept "solvability" is defined in such a way that consistency of the implicit system equations is locally guaranteed for all input sequences, and an algorithm is introduced to verify the solvability of an implicit system in that sense. It is demonstrated how this mechanism may be used to decide on the right-invertibility or functional reproducibility of a given system. In contrast to previous work on right-invertibility for special classes of implicit nonlinear systems, the approach is not restricted to the characterization of right-invertibility, but it is shown in addition how an inverse system can actually be obtained. The theory is illustrated by a realistic economic example in which the inversion procedure is applied using formula manipulation.