In this talk the problems of solvability and
right-invertibility for implicit nonlinear discrete-time control 
systems are addressed. 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