Combination of Constraint Solving Techniques: An Algebraic Point of View

Franz BaaderFranz Baader, K.U. SchulzK.U. Schulz

Franz Baader, K.U. Schulz
Combination of Constraint Solving Techniques: An Algebraic Point of View
Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Artificial Intelligence, 352-366, 1995. Springer

Details
Bibtex

KurzfassungAbstract
In a previous paper we have introduced a method that allows one to combine decision procedures for unifiability in disjoint equational theories. Lately, it has turned out that the prerequisite for this method to apply---namely that unification with so-called linear constant restrictions is decidable in the single theories---is equivalent to requiring decidability of the positive fragment of the first order theory of the equational theories. Thus, the combination method can also be seen as a tool for combining decision procedures for positive theories of free algebras defined by equational theories. The present paper uses this observation as the starting point of a more abstract, algebraic approach to formulating and solving the combination problem. Its contributions are twofold. As a new result, we describe an optimization and an extension of our combination method to the case of constraint solvers that also take relational constraints (such as ordering constraints) into account. The second contribution is a new proof method, which depends on abstract notions and results from universal algebra, as opposed to technical manipulations of terms (such as ordered rewriting, abstraction functions, etc.)
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderSchulz-RTA-95,
  address = {Kaiserslautern, Germany},
  author = {F. {Baader} and K.U. {Schulz}},
  booktitle = {Proceedings of the 6th International Conference on Rewriting Techniques and Applications},
  pages = {352--366},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Combination of Constraint Solving Techniques: {A}n Algebraic Point of View},
  volume = {914},
  year = {1995},
}