On using ground joinable equations in equational theorem proving

When rewriting and completion techniques are used for equational theorem proving, the axiom set is saturated with the aim to get a rewrite system that is terminating and confluent on ground terms. To reduce the computational effort it should (1) be powerful for rewriting and (2) create not too many critical pairs. These problems become especially important if some operators are associative and commutative (AC). We show in this paper how these two goals can be reached to some extent by using ground joinable equations for simplification purposes and omitting them from the generation of new facts. For the special case of AC-operators we present a simple redundancy criterion which is easy to implement, efficient, and effective in practice, leading to significant speed-ups.