|
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 ACRPO is the AC-compatible total reduction ordering of [16]), which was a missing ingredient for automated deduction strategies with AC-constraint inheritance [15, 19]. As in the AC-unification case (actually the AC-unification algorithm of [9] 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., |
