Associative-Commutative Operators

Saturate provides two ways of dealing with AC-operators. One is by the standard methods of ordered rewriting. This is in many cases not good enough. On problems in which AC-symbols play a central role and interact non-trivially with some transitive relation, ordered rewriting as provided in Saturate may perform poorly, although AC-specific redundancy proof techniques (e.g., convergence tests for critical pairs by case analysis and constrained rewriting) are provided. A non-trivial case in which ordered rewriting together with these techniques works well is an exampe due to Overbeek. In that example, saturation not only finds the required commutativity property of multiplication but moreover terminates with a ground convergent system for the commutative ring in question.

Alternatively, and this is the standard setting, Saturate will apply AC-superposition and AC-chaining based on AC-unification, extended clauses and AC-orderings as explained in (Bachmair & Ganzinger, 1995 a). AC-unification can be very expensive. Most of the time, additional algebraic structure e.g., cancellativity, group or ring structure, is present and, hence, should be exploited. This is one of the directions into which future research concentrates on.

Imprint | Data Protection