Although new matching algorithms for (among other theories) associativity, associativity + commutativity, and associativity + commutativity + identity are presented, the emphasis is not so much on individual theories but on the general method of proof transformation as a tool for showing the equivalence of different proof systems.
After studying proof translations defined by rewriting systems, equivalence tests based on the notion of {\em resolvant} theories are used to derive new matching and in some cases unification procedures for a number of equational theories. Finally the combination of resolvant systems is investigated.
BibTeX: