In symbolic integration, the Risch-Norman algorithm tries to find the closed forms of elementary integrals over differential fields based on heuristic degree bounds. Norman presented an approach that avoids degree bounds and only relies on the completion of reduction systems. We give a formalization of complete reduction systems and develop a refined algorithm with a proof of correctness, which terminates in more instances. In some situations, when the algorithm cannot terminate, we can also find infinite reduction systems that are complete. We present such infinite systems for the fields generated by Airy functions, complete elliptic integrals, and solutions of certain second-order linear differential equations, respectively.
Moreover, complete reduction systems can be used to find rigorous degree bounds. We give a general formula for the weighted degree bounds and also find tight bounds for above examples.