  We further develop the theoretical framework of proof mining, a program in
mathematical logic that seeks to quantify and extract computational information
from prima facie `non-computational' proofs from the mainstream literature. To
that end, we establish logical metatheorems that allow for the treatment of
proofs involving nonlinear semigroups generated by an accretive operator,
structures which in particular arise in the study of the solutions and
asymptotic behavior of partial differential equations. In that way, the here
established metatheorems facilitate a theoretical basis for the application of
methods from the proof mining program to the wide variety of mathematical
results established in the context of that theory since the 1960's. We in
particular illustrate the applicability of the new systems and their
metatheorems introduced here by providing two case studies on two central
results due to Reich and Plant, respectively, on the asymptotic behavior of
said semigroups and the resolvents of their generators where we derive rates of
convergence for the limits involved which are, moreover, polynomial in all
data.
