Orderings, AC-Theories and Symbolic Constraint Solving

Abstract

We design combination techniques for symbolic constraint solving in the presence of associative and commutative (AC) function symbols. This yields an algorithm for solving AC-RPO constraints (where AC-RPO is the AC-compatible total reduction ordering introduced By R. Nieuwenhuis and A. Rubio in 1993), which was a missing ingredient for automated deduction strategies with AC-constraint inheritance. As in the AC-unification case (actually the AC-unification algorithm of Kapur and Narendran is an instance of ours), for this purpose we first study the pure case, i.e. we show how to solve AC-ordering constraints built over a single AC function symbol and variables. Since AC-RPO is an interpretation-based ordering, our algorithm also requires the combination of algorithms for solving interpreted constraints and non-interpreted constraints.

paper (.ps version)