A method for simplification procedure design based on formula rewriting systems

We generalize the notion of formula rewriting systems proposed in the prelim¬inary work, extend the class of such systems and expand our previous results for the new class. We demonstrate that the well-known techniques of formula simpli¬fication can be represented in terms of this formalism and investigate termination problem for such systems in detail.