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)