Combining Symbolic Constraint Solvers on Algebraic Domains

In the context of constraint logic programming and theorem proving, the development of constraint solvers on algebraic domains and their combination is of prime interest. As an example, a constraint solver in finite algebras is presented for a constraint language including for instance equations, disequations and inequations. By extending techniques used for the combination of unification in disjoint equational theories, we show how to combine constraint solvers on different algebraic domains that may share some constant symbols. We illustrate this technique by combining the constraint solver in finite algebras with other unification algorithms, and with another constraint solver on a different finite algebra.