This thesis is devoted to the combination of constraint solvers. Deduction with constraints is a way to get more efficient deduction systems thanks to constraints which must be satisfied for applying general deduction rules like resolution, superposition or simplification. Deduction systems usually integrate several computation domains like terms, integers, Booleans, finite sets or algebras, but actually without cooperation of related constraint solvers. The combination problem consists of extending the use of constraint solvers in order to solve mixed constraints on the union of computation domains and so to get more expressive deduction systems. A particularly important example is the combination of unification algorithms where constraints are equations and computation domains are disjoint equational theories.
In this thesis, we generalize the use of combination techniques to constraint solving. We present unification algorithms for non-disjoint equational theories where some combination techniques are still available. For matching algorithms, we introduce the optimal class of so-called partially linear theories where the combination problem can be solved without introducing unification problems. Most of our combined algorithms for unification, matching or word-problem can be used to decide solvability of these problems, which is of greatest interest for constraint logic programming. We propose a framework for combining symbolic constraint solvers. The related solver and combined constraint language are illustrated by the combination of constraint solvers in finite algebras and used for the integration of a built-in structure into the general mechanism of constraint narrowing.