zbMATH — the first resource for mathematics

Combining symbolic constraint solvers on algebraic domains. (English) Zbl 0819.68111
Summary: 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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
68N17 Logic programming
Full Text: DOI