Normalization for symbolic equation-solving systems
B. D. Parrello · 1990
In recent years, more and more attention has been focused on the use of symbolic, rather than numerical, techniques for solving systems of nonlinear equations. A key component of any symbolic equation-solving technique is the use of rewrite rules, called normalization rules, to simplify equations, reduce the complexity of the equation-solving algorithms, and more effectively incorporate the results of solving a particular equation into the unsolved equations. In this dissertation, a hierarchy of normalization rules is proposed for use in symbolic equation-solving systems. The first set of rules imposes a rigid structure on the equations in order to simplify the equation-solving algorithms. The second set of rules builds on the first to produce a normal form that is canonical with respect to associativity, distributivity, commutativity, and combination and cancellation of addends. It is also shown that the normal form thus produced will automatically evaluate any expression containing no variables. The third set of rules incorporates combination and cancellation of factors. It is shown that this set of rules does not produce a normal form. A theorem-prover is used to produce many of the proofs, including those of canonicality, termination, and correctness of the rewrite rules.